src/HOL/Tools/function_package/fundef_package.ML
changeset 21491 574e63799847
parent 21435 883337ea2f3b
child 21511 16c62deb1adf
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Nov 23 18:49:55 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Nov 23 20:33:25 2006 +0100
     1.3 @@ -88,8 +88,8 @@
     1.4  
     1.5        
     1.6      in
     1.7 -      lthy
     1.8 -        |> LocalTheory.declaration (add_fundef_data defname cdata) (* save in target *)
     1.9 +      lthy  (* FIXME proper handling of morphism *)
    1.10 +        |> LocalTheory.declaration (fn phi => add_fundef_data defname cdata) (* save in target *)
    1.11          |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
    1.12      end (* FIXME: Add cases for induct and cases thm *)
    1.13