# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256814571 -3600
# Node ID 7affee8f90f5f8f5ac55d556d003ba985e630592
# Parent  811f17de4031e765ae413a392a296222368737f1
Using subst for identity definition.

diff -r 811f17de4031 -r 7affee8f90f5 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 29 08:46:34 2009 +0100
+++ b/QuotMain.thy	Thu Oct 29 12:09:31 2009 +0100
@@ -650,6 +650,45 @@
   make_const_def nconst_bname otrm mx [(qty, rty)] lthy
 *}
 
+text {* Does the same as 'subst' in a given prop or theorem *}
+ML {*
+fun eqsubst_prop ctxt thms t =
+  let
+    val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_prop"
+    | SOME th => cprem_of th 1
+  in term_of a' end
+*}
+
+ML {*
+  fun repeat_eqsubst_prop ctxt thms t =
+    repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
+    handle _ => t
+*}
+
+
+ML {*
+fun eqsubst_thm ctxt thms thm =
+  let
+    val goalstate = Goal.init (Thm.cprop_of thm)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_thm"
+    | SOME th => cprem_of th 1
+    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
+    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
+  in
+    @{thm Pure.equal_elim_rule1} OF [rt,thm]
+  end
+*}
+
+ML {*
+  fun repeat_eqsubst_thm ctxt thms thm =
+    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+    handle _ => thm
+*}
+
 ML {*
 fun build_repabs_term lthy thm constructors rty qty =
   let
@@ -702,7 +741,7 @@
         else list_comb(opp, tms)
       end
   in
-    MetaSimplifier.rewrite_term @{theory} @{thms id_def_sym} []
+    repeat_eqsubst_prop lthy @{thms id_def_sym}
       (build_aux lthy (Thm.prop_of thm))
   end
 *}
@@ -831,28 +870,6 @@
 
 section {* Cleaning the goal *}
 
-text {* Does the same as 'subst' in a given theorem *}
-ML {*
-fun eqsubst_thm ctxt thms thm =
-  let
-    val goalstate = Goal.init (Thm.cprop_of thm)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      NONE => error "eqsubst_thm"
-    | SOME th => cprem_of th 1
-    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
-    val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'))
-    val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac));
-  in
-    @{thm Pure.equal_elim_rule1} OF [rt,thm]
-  end
-*}
-
-ML {*
-  fun repeat_eqsubst_thm ctxt thms thm =
-    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
-    handle _ => thm
-*}
-
 text {* expects atomized definition *}
 ML {*
   fun add_lower_defs_aux ctxt thm =