subtype.ML

--- a/subtype.ML	Wed Nov 23 10:37:27 1994 +0100
+++ b/subtype.ML	Wed Nov 23 10:41:42 1994 +0100
@@ -65,15 +65,16 @@
 
     val Rep_name = "Rep_" ^ name;
     val Abs_name = "Abs_" ^ name;
+    val setC = Const (name, setT);
     val RepC = Const (Rep_name, newT --> oldT);
     val AbsC = Const (Abs_name, oldT --> newT);
     val x_new = Free ("x", newT);
     val y_old = Free ("y", oldT);
 
     (*axioms*)
-    val rep_type = mk_Trueprop (mk_mem (RepC $ x_new, set));
+    val rep_type = mk_Trueprop (mk_mem (RepC $ x_new, setC));
     val rep_type_inv = mk_Trueprop (mk_eq (AbsC $ (RepC $ x_new), x_new));
-    val abs_type_inv = mk_implies (mk_Trueprop (mk_mem (y_old, set)),
+    val abs_type_inv = mk_implies (mk_Trueprop (mk_mem (y_old, setC)),
       mk_Trueprop (mk_eq (RepC $ (AbsC $ y_old), y_old)));
 
 
@@ -110,8 +111,11 @@
      [(tname, replicate tlen logicS, logicS),
       (tname, replicate tlen termS, termS)]
     |> add_consts_i
-     [(Rep_name, newT --> oldT, NoSyn),
+     [(name, setT, NoSyn),
+      (Rep_name, newT --> oldT, NoSyn),
       (Abs_name, oldT --> newT, NoSyn)]
+    |> add_defs_i
+     [(name ^ "_def", mk_equals (setC, set))]
     |> add_axioms_i
      [(Rep_name, rep_type),
       (Rep_name ^ "_inverse", rep_type_inv),