src/HOL/Tools/function_package/fundef_package.ML
changeset 22623 5fcee5b319a2
parent 22498 62cdd4b3e96b
child 22635 d33735c0f225
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Apr 10 14:11:01 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Apr 10 18:09:58 2007 +0200
     1.3 @@ -69,6 +69,8 @@
     1.4      end
     1.5  
     1.6  
     1.7 +fun pr_ctxdata (x: fundef_context_data) = (Output.debug (K (PolyML.makestring x)); x)
     1.8 +
     1.9  fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
    1.10      let
    1.11        val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.12 @@ -89,9 +91,10 @@
    1.13  
    1.14        val cdata = FundefCtxData { add_simps=addsmps, psimps=psimps',
    1.15                                    pinducts=snd pinducts', termination=termination', f=f, R=R }
    1.16 +            |> morph_fundef_data (LocalTheory.target_morphism lthy)
    1.17      in
    1.18 -      lthy  (* FIXME proper handling of morphism *)
    1.19 -        |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
    1.20 +      lthy 
    1.21 +        |> LocalTheory.declaration (fn phi => add_fundef_data defname (pr_ctxdata (morph_fundef_data phi cdata))) (* save in target *)
    1.22          |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
    1.23      end (* FIXME: Add cases for induct and cases thm *)
    1.24