src/Pure/sign.ML
changeset 922 196ca0973a6d
parent 901 77795af99315
child 926 9d1348498c36
--- a/src/Pure/sign.ML	Thu Mar 02 12:07:20 1995 +0100
+++ b/src/Pure/sign.ML	Fri Mar 03 11:48:05 1995 +0100
@@ -61,7 +61,9 @@
     val add_name: string -> sg -> sg
     val make_draft: sg -> sg
     val merge: sg * sg -> sg
+    val proto_pure: sg
     val pure: sg
+    val cpure: sg
     val const_of_class: class -> string
     val class_of_const: string -> class
   end
@@ -179,10 +181,16 @@
 
 (** pretty printing of terms and types **)
 
-fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
+fun pretty_term (Sg {syn, stamps, ...}) =
+  let val curried = "CPure" mem (map ! stamps);
+  in Syntax.pretty_term curried syn end;
+
 fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
 
-fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
+fun string_of_term (Sg {syn, stamps, ...}) = 
+  let val curried = "CPure" mem (map ! stamps);
+  in Syntax.string_of_term curried syn end;
+
 fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
 
 fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
@@ -516,7 +524,7 @@
 
 (** the Pure signature **)
 
-val pure =
+val proto_pure =
   make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#"
   |> add_types
    (("fun", 2, NoSyn) ::
@@ -537,7 +545,24 @@
     ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("TYPE", "'a itself", NoSyn)]
+  |> add_name "ProtoPure";
+
+val pure = proto_pure
+  |> add_syntax
+   [("_appl",     "[('b => 'a), args] => logic",    Mixfix ("(1_/(1'(_')))",
+                                                    [max_pri, 0], max_pri)),
+    ("_appl",     "[('b => 'a), args] => aprop",    Mixfix ("(1_/(1'(_')))",
+                                                    [max_pri, 0], max_pri))]
   |> add_name "Pure";
 
+val cpure = proto_pure
+  |> add_syntax
+   [("_applC",     "[('b => 'a), 'c] => logic",     Mixfix ("(1_ (1_))",
+                                                    [max_pri-1, max_pri],
+                                                    max_pri-1)),
+    ("_applC",     "[('b => 'a), 'c] => aprop",     Mixfix ("(1_ (1_))",
+                                                    [max_pri-1, max_pri],
+                                                    max_pri-1))]
+  |> add_name "CPure";
 
 end;