# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259286956 -3600
# Node ID 6b59a3844055c4ffd69750f8bdf39f3f05016dc5
# Parent  1056861b562c7b45218c8be9b3d06dd8d5508b26
introduced a separate lemma for id_simps

diff -r 1056861b562c -r 6b59a3844055 IntEx.thy
--- a/IntEx.thy	Fri Nov 27 02:45:54 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 02:55:56 2009 +0100
@@ -212,7 +212,7 @@
 *}
 
 ML {* 
-mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
+inj_repabs_trm @{context} (reg_atrm, aqtrm) 
   |> Syntax.check_term @{context}
 *}
 
@@ -226,7 +226,7 @@
 done
 
 ML {*
-inj_REPABS @{context} (reg_atrm, aqtrm)  
+inj_repabs_trm @{context} (reg_atrm, aqtrm)  
 |> Syntax.string_of_term @{context}
 |> writeln
 *}
diff -r 1056861b562c -r 6b59a3844055 QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 02:45:54 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 02:55:56 2009 +0100
@@ -219,15 +219,14 @@
 apply (simp_all)
 done
 
+lemmas id_simps =
+  FUN_MAP_I[THEN eq_reflection]
+  id_apply[THEN eq_reflection]
+  id_def_sym prod_fun_id map_id
+
 ML {*
-fun simp_ids lthy thm =
-let 
-  val thms = @{thms eq_reflection[OF FUN_MAP_I] 
-                    eq_reflection[OF id_apply] 
-                    id_def_sym prod_fun_id map_id} 
-in
-  MetaSimplifier.rewrite_rule thms thm
-end
+fun simp_ids thm =
+  MetaSimplifier.rewrite_rule @{thms id_simps} thm
 *}
 
 section {* Debugging infrastructure for testing tactics *}
@@ -271,11 +270,11 @@
   let
     val e1 = @{thm fun_cong} OF [thm];
     val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
-    val g = simp_ids lthy f
+    val g = simp_ids f
   in
-    (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
+    (simp_ids thm) :: (add_lower_defs_aux lthy g)
   end
-  handle _ => [simp_ids lthy thm]
+  handle _ => [simp_ids thm]
 *}
 
 ML {*
@@ -732,18 +731,13 @@
 
 ML {*
 fun quotient_tac quot_thm =
-let
-  val simps = @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] 
-                     id_def_sym prod_fun_id map_id}
-in
   REPEAT_ALL_NEW (FIRST' [
     rtac @{thm FUN_QUOTIENT},
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
     (* For functional identity quotients, (op = ---> op =) *)
-    CHANGED' (simp_tac (HOL_ss addsimps simps))
+    CHANGED' (simp_tac (HOL_ss addsimps @{thms id_simps}))
   ])
-end
 *}
 
 ML {*
@@ -917,6 +911,7 @@
     val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply});
     val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
     val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t;
+                                              (* FIXME/TODO: should that be id_simps? *)
   in
     singleton (ProofContext.export lthy' lthy) t_id
   end