src/HOL/Tools/function_package/fundef_package.ML
changeset 25169 b1ea9d2e6a72
parent 25088 9a13ab12b174
child 25201 e6fe58b640ce
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 24 17:17:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Oct 24 18:30:06 2007 +0200
     1.3 @@ -80,11 +80,9 @@
     1.4  
     1.5        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
     1.6                                    pinducts=snd pinducts', termination=termination', fs=fs, R=R, defname=defname }
     1.7 -      val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
     1.8      in
     1.9        lthy 
    1.10 -        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata)) (* save in target *)
    1.11 -        |> Context.proof_map (add_fundef_data cdata') (* also save in local context *)
    1.12 +        |> LocalTheory.declaration (fn phi => add_fundef_data (morph_fundef_data phi cdata))
    1.13      end (* FIXME: Add cases for induct and cases thm *)
    1.14  
    1.15