declarations: pass morphism (dummy);
authorwenzelm
Thu Nov 23 20:33:25 2006 +0100 (2006-11-23)
changeset 21491574e63799847
parent 21490 2f83b11c301b
child 21492 c73faa8e98aa
declarations: pass morphism (dummy);
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
     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  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Nov 23 18:49:55 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Nov 23 20:33:25 2006 +0100
     2.3 @@ -704,8 +704,8 @@
     2.4         induct = induct'}
     2.5  
     2.6    in
     2.7 -    (result, LocalTheory.declaration
     2.8 -       (put_inductives cnames ({names = cnames, coind = coind}, result)) ctxt4)
     2.9 +    (result, LocalTheory.declaration (fn phi => (* FIXME *)
    2.10 +       (put_inductives cnames ({names = cnames, coind = coind}, result))) ctxt4)
    2.11    end;
    2.12  
    2.13