fun command: use "reinit" between "function" and "termination"
authorkrauss
Wed Oct 24 18:30:06 2007 +0200 (2007-10-24)
changeset 25169b1ea9d2e6a72
parent 25168 2650a4a6ad3e
child 25170 bd06fd396fd0
fun command: use "reinit" between "function" and "termination"
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Oct 24 17:17:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Oct 24 18:30:06 2007 +0200
     1.3 @@ -300,6 +300,7 @@
     1.4      lthy
     1.5        |> FundefPackage.add_fundef fixes statements config flags
     1.6        |> by_pat_completeness_simp
     1.7 +      |> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of lthy))
     1.8        |> termination_by_lexicographic_order
     1.9  
    1.10  val _ =
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 24 17:17:43 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 24 18:30:06 2007 +0200
     2.3 @@ -80,11 +80,9 @@
     2.4  
     2.5        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
     2.6                                    pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
     2.7 -      val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
     2.8      in
     2.9        lthy 
    2.10 -        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata)) (* save in target *)
    2.11 -        |> Context.proof_map (add_fundef_data cdata') (* also save in local context *)
    2.12 +        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata))
    2.13      end (* FIXME: Add cases for induct and cases thm *)
    2.14  
    2.15