# HG changeset patch
# User wenzelm
# Date 750084904 -3600
# Node ID d981488bda7b541d25ce07e0e8c0d461717c0e91
# Parent  97aae241094b253194179a7497f2f7f3f3904d55
*** empty log message ***

diff -r 97aae241094b -r d981488bda7b src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Fri Oct 08 12:35:53 1993 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Fri Oct 08 13:55:04 1993 +0100
@@ -5,8 +5,6 @@
 This file builds the syntax module.
 *)
 
-use "lib.ML";   (* FIXME *)
-
 use "pretty.ML";
 
 use "ast.ML";
diff -r 97aae241094b -r d981488bda7b src/Pure/Syntax/extension.ML
--- a/src/Pure/Syntax/extension.ML	Fri Oct 08 12:35:53 1993 +0100
+++ b/src/Pure/Syntax/extension.ML	Fri Oct 08 13:55:04 1993 +0100
@@ -236,7 +236,7 @@
     fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri);
 
     fun mkappl T =
-      Mfix ("_(1'(_'))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
+      Mfix ("_/(1'(_'))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);
 
     fun mkid T = Mfix ("_", idT --> T, "", [], max_pri);
 
diff -r 97aae241094b -r d981488bda7b src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Oct 08 12:35:53 1993 +0100
+++ b/src/Pure/Syntax/printer.ML	Fri Oct 08 13:55:04 1993 +0100
@@ -59,33 +59,6 @@
 
 fun ast_of_term trf show_types show_sorts tm =
   let
-(*(* FIXME old - remove *)
-    fun fix_aprop tys (Abs (x, ty, t)) = Abs (x, ty, fix_aprop (ty :: tys) t)
-      | fix_aprop tys t =
-          let
-            val (f, args) = strip_comb t;
-            val t' = list_comb (f, map (fix_aprop tys) args);
-          in
-            if not (is_Const f) andalso fastype_of (tys, t) = propT
-            then Const (apropC, dummyT) $ t' else t'
-          end;
-
-    val aprop_const = Const (apropC, dummyT);
-
-    fun fix_aprop (tm as Const _) = tm
-      | fix_aprop (tm as Free (x, ty)) =
-          if ty = propT then aprop_const $ Free (x, dummyT) else tm
-      | fix_aprop (tm as Var (xi, ty)) =
-          if ty = propT then aprop_const $ Var (xi, dummyT) else tm
-      | fix_aprop (tm as Bound _) = tm
-      | fix_aprop (Abs (x, ty, t)) = Abs (x, ty, fix_aprop t)
-      | fix_aprop (t1 $ t2) = fix_aprop t1 $ fix_aprop t2;
-
-    val fix_aprop = fn _ => fn tm => fix_aprop tm;
-*)
-
-    (* FIXME check *)
-
     fun aprop t = Const (apropC, dummyT) $ t;
 
     fun is_prop tys tm =
diff -r 97aae241094b -r d981488bda7b src/Pure/Syntax/sextension.ML
--- a/src/Pure/Syntax/sextension.ML	Fri Oct 08 12:35:53 1993 +0100
+++ b/src/Pure/Syntax/sextension.ML	Fri Oct 08 13:55:04 1993 +0100
@@ -446,7 +446,7 @@
       Mixfix   ("_/ _",       "[idt, idts] => idts",           "_idts", [1, 0], 0),
       Delimfix ("_",          "id => aprop",                   ""),
       Delimfix ("_",          "var => aprop",                  ""),
-      Mixfix   ("_'(_')",     "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),
+      Mixfix   ("_/(1'(_'))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),
       Delimfix ("PROP _",     "aprop => prop",                 "_aprop"),
       Delimfix ("_",          "prop => asms",                  ""),
       Delimfix ("_;/ _",      "[prop, asms] => asms",          "_asms"),