IsarThy.theorem_i Drule.internalK;
authorwenzelm
Sat Oct 13 20:31:34 2001 +0200 (2001-10-13)
changeset 1174086ac4189a1c1
parent 11739 c0ca4b89159c
child 11741 470e608d7a74
IsarThy.theorem_i Drule.internalK;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/typedef_package.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Oct 13 20:31:05 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Oct 13 20:31:34 2001 +0200
     1.3 @@ -594,7 +594,10 @@
     1.4      val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
     1.5      val atts = map (prep_att thy) raw_atts;
     1.6      val thms = map (smart_mk_cases thy ss) cprops;
     1.7 -  in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end;
     1.8 +  in
     1.9 +    thy |>
    1.10 +    IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)]
    1.11 +  end;
    1.12  
    1.13  val inductive_cases =
    1.14    gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
     2.1 --- a/src/HOL/Tools/recdef_package.ML	Sat Oct 13 20:31:05 2001 +0200
     2.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat Oct 13 20:31:34 2001 +0200
     2.3 @@ -310,8 +310,8 @@
     2.4        error ("No termination condition #" ^ string_of_int i ^
     2.5          " in recdef definition of " ^ quote name);
     2.6    in
     2.7 -    thy
     2.8 -    |> IsarThy.theorem_i (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
     2.9 +    thy |> IsarThy.theorem_i Drule.internalK
    2.10 +      (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
    2.11    end;
    2.12  
    2.13  val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
     3.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Oct 13 20:31:05 2001 +0200
     3.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 13 20:31:34 2001 +0200
     3.3 @@ -216,8 +216,10 @@
     3.4  (* typedef_proof interface *)
     3.5  
     3.6  fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
     3.7 -  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy;
     3.8 -  in thy |> IsarThy.theorem_i ((("", [att]), (goal, ([goal_pat], []))), comment) int end;
     3.9 +  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set thy in
    3.10 +    thy
    3.11 +    |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
    3.12 +  end;
    3.13  
    3.14  val typedef_proof = gen_typedef_proof read_term;
    3.15  val typedef_proof_i = gen_typedef_proof cert_term;
     4.1 --- a/src/Pure/axclass.ML	Sat Oct 13 20:31:05 2001 +0200
     4.2 +++ b/src/Pure/axclass.ML	Sat Oct 13 20:31:34 2001 +0200
     4.3 @@ -440,7 +440,7 @@
     4.4  
     4.5  fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
     4.6    thy
     4.7 -  |> IsarThy.theorem_i ((("", [inst_attribute add_thms]),
     4.8 +  |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]),
     4.9      (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
    4.10  
    4.11  val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;