1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 21 18:07:30 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 21 18:07:31 2006 +0100
     1.3 @@ -38,6 +38,8 @@
     1.4  open FundefLib
     1.5  open FundefCommon
     1.6  
     1.7 +val note_theorem = LocalTheory.note Thm.theoremK
     1.8 +
     1.9  fun burrow_snd f ps = (* ('a list -> 'b list) -> ('c * 'a) list -> ('c * 'b) list *)
    1.10      let val (xs, ys) = split_list ps
    1.11      in xs ~~ f ys end
    1.12 @@ -49,13 +51,16 @@
    1.13      let
    1.14        val fnames = map (fst o fst) fixes
    1.15  
    1.16 -      val (saved_spec_psimps, lthy) = fold_map (fold_map LocalTheory.note) (restore_spec_structure psimps spec) lthy
    1.17 +      val (saved_spec_psimps, lthy) =
    1.18 +        fold_map (fold_map note_theorem) (restore_spec_structure psimps spec) lthy
    1.19        val saved_psimps = flat (map snd (flat saved_spec_psimps))
    1.20  
    1.21        val psimps_by_f = FundefMutual.sort_by_function mutual_info fnames saved_psimps
    1.22  
    1.23        fun add_for_f fname psimps =
    1.24 -          LocalTheory.note ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts), psimps) #> snd
    1.25 +        note_theorem
    1.26 +          ((NameSpace.qualified fname label, Attrib.internal Simplifier.simp_add :: moreatts),
    1.27 +            psimps) #> snd
    1.28      in
    1.29        (saved_psimps,
    1.30         fold2 add_for_f fnames psimps_by_f lthy)
    1.31 @@ -73,10 +78,10 @@
    1.32        val (((psimps', pinducts'), (_, [termination'])), lthy) = 
    1.33            lthy
    1.34              |> PROFILE "adding_psimps" (add_simps "psimps" [] mutual_info fixes psimps spec)
    1.35 -            ||>> PROFILE "adding pinduct" (LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
    1.36 -            ||>> PROFILE "adding termination" (LocalTheory.note ((qualify "termination", []), [termination]))
    1.37 -            ||> (snd o PROFILE "adding cases" (LocalTheory.note ((qualify "cases", []), [cases])))
    1.38 -            ||> (snd o PROFILE "adding domintros" (LocalTheory.note ((qualify "domintros", []), domintros)))
    1.39 +            ||>> PROFILE "adding pinduct" (note_theorem ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts))
    1.40 +            ||>> PROFILE "adding termination" (note_theorem ((qualify "termination", []), [termination]))
    1.41 +            ||> (snd o PROFILE "adding cases" (note_theorem ((qualify "cases", []), [cases])))
    1.42 +            ||> (snd o PROFILE "adding domintros" (note_theorem ((qualify "domintros", []), domintros)))
    1.43  
    1.44        val cdata = FundefCtxData { fixes=fixes, spec=spec, mutual=mutual_info, psimps=psimps',
    1.45                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.46 @@ -121,7 +126,7 @@
    1.47        val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
    1.48      in
    1.49        (name, lthy
    1.50 -         |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]]
    1.51 +         |> Proof.theorem_i NONE afterqed [[(goal, [])]]
    1.52           |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
    1.53      end
    1.54  
    1.55 @@ -145,7 +150,7 @@
    1.56      in
    1.57          lthy
    1.58            |> PROFILE "adding tsimps" (add_simps "simps" [] mutual fixes tsimps spec) |> snd
    1.59 -          |> PROFILE "adding tinduct" (LocalTheory.note ((qualify "induct", []), tinduct)) |> snd
    1.60 +          |> PROFILE "adding tinduct" (note_theorem ((qualify "induct", []), tinduct)) |> snd
    1.61      end
    1.62  
    1.63  
    1.64 @@ -159,11 +164,10 @@
    1.65          val goal = FundefTermination.mk_total_termination_goal f R
    1.66      in
    1.67        lthy
    1.68 -        |> ProofContext.note_thmss_i [(("termination",
    1.69 +        |> ProofContext.note_thmss_i "" [(("termination",
    1.70                                          [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
    1.71          |> set_termination_rule termination
    1.72 -        |> Proof.theorem_i PureThy.internalK NONE
    1.73 -                           (total_termination_afterqed name data) [[(goal, [])]]
    1.74 +        |> Proof.theorem_i NONE (total_termination_afterqed name data) [[(goal, [])]]
    1.75      end
    1.76  
    1.77