# HG changeset patch
# User paulson
# Date 835107458 -7200
# Node ID 0eef167ebe1bd0d803390064ed3431ea0dd00406
# Parent  8cb50df4957093d797476972e2afbd661f88b067
Translation infixes <->, etc., no longer available at top-level

diff -r 8cb50df49570 -r 0eef167ebe1b src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Mon Jun 17 16:51:47 1996 +0200
+++ b/src/HOL/datatype.ML	Tue Jun 18 16:17:38 1996 +0200
@@ -224,8 +224,8 @@
       
       val xrules =
         let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
-        in [("logic", "case x of " ^ first_part) <->
-             ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
+        in [Syntax.<-> (("logic", "case x of " ^ first_part),
+			("logic", tname ^ "_case " ^ scnd_part ^ " x"))]
         end;
 
      (*type declarations for constructors*)
diff -r 8cb50df49570 -r 0eef167ebe1b src/HOLCF/ax_ops/thy_ops.ML
--- a/src/HOLCF/ax_ops/thy_ops.ML	Mon Jun 17 16:51:47 1996 +0200
+++ b/src/HOLCF/ax_ops/thy_ops.ML	Tue Jun 18 16:17:38 1996 +0200
@@ -153,53 +153,70 @@
   | syn_decls curried sign (_::tl) = syn_decls curried sign tl
   | syn_decls _ _ [] = [];
 
+fun translate name vars rhs = 
+    Syntax.<-> ((Ast.mk_appl (Constant (mk_internal_name name)) 
+		 (map Variable vars)), 
+		rhs); 
+
 (* generating the translation rules. Called by add_ext_axioms(_i) *)
 local open Ast in 
 fun xrules_of true ((name,typ,CInfixl(i))::tail) = 
-    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
-     (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
-      Constant (mk_internal_name name),Variable "A"]),Variable "B"]))
+    translate name ["A","B"]
+     (mk_appl (Constant "@fapp") 
+      [(mk_appl (Constant "@fapp") 
+	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
     ::xrules_of true tail
   | xrules_of true ((name,typ,CInfixr(i))::tail) = 
-    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
-     (mk_appl (Constant "@fapp") [(mk_appl (Constant "@fapp") [
-      Constant (mk_internal_name name),Variable "A"]),Variable "B"]))
+    translate name ["A","B"]
+     (mk_appl (Constant "@fapp") 
+      [(mk_appl (Constant "@fapp") 
+	[Constant (mk_internal_name name),Variable "A"]),Variable "B"])
     ::xrules_of true tail
 (*####*)
-  | xrules_of true ((name,typ,CMixfix(_))::tail) = let
-        fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
-        |   argnames _ _ = [];
-        val names = argnames (ord"A") typ;
-        in if names = [] then [] else [mk_appl (Constant name) (map Variable names)<->
-            foldl (fn (t,arg) => (mk_appl (Constant "@fapp") [t,Variable arg]))
-                  (Constant name,names)] end
+  | xrules_of true ((name,typ,CMixfix(_))::tail) = 
+        let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
+            |   argnames _ _ = [];
+            val names = argnames (ord"A") typ;
+        in if names = [] then [] else 
+	    [Syntax.<-> (mk_appl (Constant name) (map Variable names),
+			 foldl (fn (t,arg) => 
+				(mk_appl (Constant "@fapp") [t,Variable arg]))
+			 (Constant name,names))] 
+        end
     @xrules_of true tail
 (*####*)
   | xrules_of false ((name,typ,CInfixl(i))::tail) = 
-    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
+    translate name ["A","B"]
     (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
-     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]))
+     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
     ::xrules_of false tail
   | xrules_of false ((name,typ,CInfixr(i))::tail) = 
-    ((mk_appl (Constant (mk_internal_name name)) [Variable "A",Variable "B"]) <->
+    translate name ["A","B"]
     (mk_appl (Constant "@fapp") [ Constant(mk_internal_name name),
-     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])]))
+     (mk_appl (Constant "@ctuple") [Variable "A",Variable "B"])])
     ::xrules_of false tail
 (*####*)
-  | xrules_of false ((name,typ,CMixfix(_))::tail) = let
-        fun foldr' f l =
-          let fun itr []  = raise LIST "foldr'"
-                | itr [a] = a
-                | itr (a::l) = f(a, itr l)
-          in  itr l end;
-        fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
-        |   argnames n _ = [chr n];
-        val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
-                                             | _ => []);
-        in if vars = [] then [] else [mk_appl (Constant name) vars <->
-            (mk_appl (Constant "@fapp") [Constant name, case vars of [v] => v
-                | args => mk_appl (Constant "@ctuple") [hd args,foldr' (fn (t,arg) => 
-                                mk_appl (Constant "_args") [t,arg]) (tl args)]])]
+  | xrules_of false ((name,typ,CMixfix(_))::tail) = 
+        let fun foldr' f l =
+	      let fun itr []  = raise LIST "foldr'"
+		    | itr [a] = a
+		    | itr (a::l) = f(a, itr l)
+	      in  itr l end;
+	    fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
+	    |   argnames n _ = [chr n];
+	    val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
+						 | _ => []);
+        in if vars = [] then [] else 
+	    [Syntax.<-> 
+	     (mk_appl (Constant name) vars,
+	      mk_appl (Constant "@fapp")
+	      [Constant name, 
+	       case vars of [v] => v
+	                 | args => mk_appl (Constant "@ctuple")
+			             [hd args,
+				      foldr' (fn (t,arg) => 
+					      mk_appl (Constant "_args")
+					      [t,arg]) (tl args)]])]
         end
     @xrules_of false tail
 (*####*)
diff -r 8cb50df49570 -r 0eef167ebe1b src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Jun 17 16:51:47 1996 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Tue Jun 18 16:17:38 1996 +0200
@@ -311,12 +311,15 @@
   optional ("(" $$-- !! (name --$$ ")")) "\"logic\"" -- string >> mk_pair;
 
 val trans_arrow =
-  $$ "=>" >> K " |-> " ||
-  $$ "<=" >> K " <-| " ||
-  $$ "==" >> K " <-> ";
+  $$ "=>" >> K "Syntax.|-> " ||
+  $$ "<=" >> K "Syntax.<-| " ||
+  $$ "==" >> K "Syntax.<-> ";
 
-val trans_decls = repeat1 (trans_pat ^^ !! (trans_arrow ^^ trans_pat))
-  >> mk_big_list;
+val trans_line =
+    trans_pat -- !! (trans_arrow -- trans_pat) >>
+        (fn (left, (arr, right)) => arr ^ "(" ^ left ^ ",\t" ^ right ^ ")");
+
+val trans_decls = repeat1 trans_line >> mk_big_list;
 
 
 (* ML translations *)
diff -r 8cb50df49570 -r 0eef167ebe1b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jun 17 16:51:47 1996 +0200
+++ b/src/Pure/sign.ML	Tue Jun 18 16:17:38 1996 +0200
@@ -55,8 +55,8 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (ast list -> ast)) list -> sg -> sg
-  val add_trrules: (string * string) trrule list -> sg -> sg
-  val add_trrules_i: ast trrule list -> sg -> sg
+  val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
+  val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   val add_name: string -> sg -> sg
   val make_draft: sg -> sg
   val merge: sg * sg -> sg