# HG changeset patch
# User wenzelm
# Date 974149189 -3600
# Node ID 474263d290576c42bb7b64a595b531842e645068
# Parent  adf901eb9c4031e61fdb7192a88a57d94e6911a0
tuned IsarThy.theorem_i;

diff -r adf901eb9c40 -r 474263d29057 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Mon Nov 13 10:34:32 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Mon Nov 13 21:59:49 2000 +0100
@@ -239,7 +239,7 @@
     val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
   in
     thy
-    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef],
+    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
       (goal, ([goal_pat], []))), comment) int
   end;
 
diff -r adf901eb9c40 -r 474263d29057 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Nov 13 10:34:32 2000 +0100
+++ b/src/Pure/axclass.ML	Mon Nov 13 21:59:49 2000 +0100
@@ -439,7 +439,7 @@
 
 fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
   thy
-  |> IsarThy.theorem_i (("", [inst_attribute add_thms],
+  |> IsarThy.theorem_i ((("", [inst_attribute add_thms]),
     (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
 
 val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;