src/HOL/Tools/function_package/fundef_package.ML
changeset 21240 8e75fb38522c
parent 21237 b803f9870e97
child 21255 617fdb08abe9
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 02:13:02 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 09:08:54 2006 +0100
     1.3 @@ -73,7 +73,8 @@
     1.4          |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
     1.5          |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
     1.6          |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
     1.7 -        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec)))
     1.8 +        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
     1.9 +        |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
    1.10      end (* FIXME: Add cases for induct and cases thm *)
    1.11  
    1.12