IsarThy.theorem_i: no locale;
authorwenzelm
Wed Oct 31 21:59:07 2001 +0100 (2001-10-31 ago)
changeset 120041703de633aaf
parent 12003 c09427e5f554
child 12005 291593391010
IsarThy.theorem_i: no locale;
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/typedef_package.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Oct 31 21:58:04 2001 +0100
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Wed Oct 31 21:59:07 2001 +0100
     1.3 @@ -310,7 +310,7 @@
     1.4        error ("No termination condition #" ^ string_of_int i ^
     1.5          " in recdef definition of " ^ quote name);
     1.6    in
     1.7 -    thy |> IsarThy.theorem_i Drule.internalK
     1.8 +    thy |> IsarThy.theorem_i Drule.internalK None
     1.9        (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
    1.10    end;
    1.11  
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Oct 31 21:58:04 2001 +0100
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 31 21:59:07 2001 +0100
     2.3 @@ -244,7 +244,8 @@
     2.4        prepare_typedef prep_term true name typ set opt_morphs thy;
     2.5      val att = #1 o att_result;
     2.6    in
     2.7 -    thy |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
     2.8 +    thy |> IsarThy.theorem_i Drule.internalK None
     2.9 +      ((("", [att]), (goal, ([goal_pat], []))), comment) int
    2.10    end;
    2.11  
    2.12  val typedef_proof = gen_typedef_proof read_term;
     3.1 --- a/src/Pure/axclass.ML	Wed Oct 31 21:58:04 2001 +0100
     3.2 +++ b/src/Pure/axclass.ML	Wed Oct 31 21:59:07 2001 +0100
     3.3 @@ -423,7 +423,7 @@
     3.4  
     3.5  fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
     3.6    thy
     3.7 -  |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
     3.8 +  |> IsarThy.theorem_i Drule.internalK None ((("", [inst_attribute add_thms]),
     3.9      (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
    3.10  
    3.11  val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;