removed debugging code
authorkrauss
Wed Apr 11 09:40:29 2007 +0200 (2007-04-11)
changeset 22635d33735c0f225
parent 22634 399e4b4835da
child 22636 c40465deaf20
removed debugging code
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Apr 11 08:28:15 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Apr 11 09:40:29 2007 +0200
     1.3 @@ -68,9 +68,6 @@
     1.4         fold2 add_for_f fnames simps_by_f lthy)
     1.5      end
     1.6  
     1.7 -
     1.8 -fun pr_ctxdata (x: fundef_context_data) = (Output.debug (K (PolyML.makestring x)); x)
     1.9 -
    1.10  fun fundef_afterqed config fixes spec defname cont sort_cont [[proof]] lthy =
    1.11      let
    1.12        val FundefResult {f, R, psimps, trsimps, subset_pinducts, simple_pinducts, termination, domintros, cases, ...} = 
    1.13 @@ -94,7 +91,7 @@
    1.14              |> morph_fundef_data (LocalTheory.target_morphism lthy)
    1.15      in
    1.16        lthy 
    1.17 -        |> LocalTheory.declaration (fn phi => add_fundef_data defname (pr_ctxdata (morph_fundef_data phi cdata))) (* save in target *)
    1.18 +        |> LocalTheory.declaration (fn phi => add_fundef_data defname (morph_fundef_data phi cdata)) (* save in target *)
    1.19          |> Context.proof_map (add_fundef_data defname cdata) (* also save in local context *)
    1.20      end (* FIXME: Add cases for induct and cases thm *)
    1.21