data declaration: removed obsolete target_morphism (still required for local data!?);
authorwenzelm
Sat Apr 14 00:46:18 2007 +0200 (2007-04-14)
changeset 226688183ee579232
parent 22667 cbfb899dd674
child 22669 62857ad97cca
data declaration: removed obsolete target_morphism (still required for local data!?);
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 14 00:46:17 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 14 00:46:18 2007 +0200
     1.3 @@ -88,11 +88,11 @@
     1.4  
     1.5        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
     1.6                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
     1.7 -            |> morph_fundef_data (LocalTheory.target_morphism lthy)
     1.8 +      val cdata' = cdata |> morph_fundef_data (LocalTheory.target_morphism lthy);  (* FIXME !? *)
     1.9      in
    1.10        lthy 
    1.11          |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *)
    1.12 -        |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
    1.13 +        |> Context.proof_map (add_fundef_data defname cdata') (* also save in local context *)
    1.14      end (* FIXME: Add cases for induct and cases thm *)
    1.15  
    1.16