src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 18:57:18 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 18:57:39 2005 +0200
@@ -371,6 +371,8 @@
 fun prep_struct (x, _, NONE) = SOME x
   | prep_struct _ = NONE;
 
+fun mk trs = map Syntax.mk_trfun trs;
+
 in
 
 fun add_syntax decls =
@@ -384,11 +386,12 @@
       val syn' = syn
         |> Syntax.extend_const_gram is_logtype ("", false) mxs_output
         |> Syntax.extend_const_gram is_logtype ("", true) mxs
-        |> Syntax.extend_trfuns ([], trs, [], []);
-    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
+        |> Syntax.extend_trfuns ([], mk trs, [], []);
+    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end);
 
 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
-  syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
+  let val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs
+  in syn |> Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs') end;
 
 end;
 
@@ -455,8 +458,6 @@
 
 in
 
-(* Read/certify type, using default sort information from context. *)
-
 val read_typ     = read_typ_aux Sign.read_typ';
 val read_typ_raw = read_typ_aux Sign.read_typ_raw';
 val cert_typ     = cert_typ_aux Sign.certify_typ;
@@ -1512,4 +1513,3 @@
 val setup = [ProofDataData.init];
 
 end;
-