Small fix: Removed the "type" sort from the abstract state type, as i…

…t's redundant and also breaks dataspace extension
isabelle-utp · Jun 29, 2023 · 3305f36 · 3305f36
1 parent 14409a1
commit 3305f36
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Lens_Lib.ML b/Lens_Lib.ML
@@ -61,7 +61,7 @@ fun lensT a b = Type (@{type_name lens_ext}, [a, b, unitT])
 fun isLensT (Type (n, _)) = (n = @{type_name lens_ext}) |
     isLensT _ = false
 
-val astateT = (TFree ("'st", [@{class type}, @{class scene_space}]))
+val astateT = (TFree ("'st", [@{class scene_space}]))
 
 fun pairWith _ [] = []
   | pairWith x (y :: ys) = [(x, y), (y, x)] @ pairWith x ys;