# HG changeset patch
# User wenzelm
# Date 1152356089 -7200
# Node ID 2b142bfb162a2cf275e7e8acf3e5637d72a75bcd
# Parent  080ca1f8afd78fcd1789872df34ae36ad3209bc2
tuned interface;

diff -r 080ca1f8afd7 -r 2b142bfb162a TFL/post.ML
--- a/TFL/post.ML	Sat Jul 08 12:54:48 2006 +0200
+++ b/TFL/post.ML	Sat Jul 08 12:54:49 2006 +0200
@@ -171,14 +171,14 @@
 
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
-       val {theory,rules,rows,TCs,full_pats_TCs} =
+       val {rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)
        val (_,[R,_]) = S.strip_comb rhs
        val dummy = Prim.trace_thms "congs =" congs
        (*the next step has caused simplifier looping in some cases*)
        val {induction, rules, tcs} =
-             proof_stage strict cs ss wfs theory
+             proof_stage strict cs ss wfs thy
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}