1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Nov 13 10:34:32 2000 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Nov 13 21:59:49 2000 +0100
     1.3 @@ -239,7 +239,7 @@
     1.4      val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
     1.5    in
     1.6      thy
     1.7 -    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef],
     1.8 +    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
     1.9        (goal, ([goal_pat], []))), comment) int
    1.10    end;
    1.11  

     2.1 --- a/src/Pure/axclass.ML	Mon Nov 13 10:34:32 2000 +0100
     2.2 +++ b/src/Pure/axclass.ML	Mon Nov 13 21:59:49 2000 +0100
     2.3 @@ -439,7 +439,7 @@
     2.4  
     2.5  fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
     2.6    thy
     2.7 -  |> IsarThy.theorem_i (("", [inst_attribute add_thms],
     2.8 +  |> IsarThy.theorem_i ((("", [inst_attribute add_thms]),
     2.9      (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
    2.10  
    2.11  val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;