# HG changeset patch
# User krauss
# Date 1176185368 -7200
# Node ID 1fb7fb24c799a277e61cf0a780ce07c364ab3d82
# Parent  4747e87ac5c4fd3ae6153d9a6b1d71c9f81c864f
removed obsolete workaround

diff -r 4747e87ac5c4 -r 1fb7fb24c799 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 09 21:28:24 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Apr 10 08:09:28 2007 +0200
@@ -350,7 +350,7 @@
 
 
 
-fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
     let
         val Globals {x, y, ranT, fvar, ...} = globals
         val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
@@ -403,9 +403,10 @@
 
 
 
-fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def =
+fun prove_stuff ctxt congs globals G f R clauses complete compat compat_store G_elim f_def =
     let
         val Globals {h, domT, ranT, x, ...} = globals
+        val thy = ProofContext.theory_of ctxt
 
         (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
         val ihyp = all domT $ Abs ("z", domT,
@@ -423,9 +424,9 @@
 
         val _ = Output.debug (K "Proving cases for unique existence...")
         val (ex1s, values) = 
-            split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+            split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
 
-        val _ = Output.debug (K "Proving: Graph is a function") (* FIXME: Rewrite this proof. *)
+        val _ = Output.debug (K "Proving: Graph is a function")
         val graph_is_function = complete
                                   |> forall_elim_vars 0
                                   |> fold (curry op COMP) ex1s
@@ -478,7 +479,7 @@
       val f_def = 
           Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
                                 Abs ("y", ranT, G $ Bound 1 $ Bound 0))
-              |> Envir.beta_norm (* FIXME: LocalTheory.def does not work if not beta-normal *)
+              |> ProofContext.cert_term lthy
 
       val ((f, (_, f_defthm)), lthy) =
         LocalTheory.def Thm.internalK ((function_name fname, mixfix), ((fdefname, []), f_def)) lthy
@@ -911,7 +912,7 @@
 
       val compat_store = store_compat_thms n compat
 
-      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
+      val (goalstate, values) = PROFILE "prove_stuff" (prove_stuff lthy congs globals G f R xclauses complete compat compat_store G_elim) f_defthm
 
       val mk_trsimps = mk_trsimps lthy globals f G R f_defthm R_elim G_induct xclauses