--- a/IntEx.thy	Tue Nov 24 14:16:57 2009 +0100
+++ b/IntEx.thy	Tue Nov 24 14:19:54 2009 +0100
@@ -180,71 +180,12 @@
   |> writeln
 *}
 
-lemma procedure: 
-  assumes a: "A"
-  and     b: "A \<Longrightarrow> B"
-  and     c: "B = C"
-  and     d: "C = D"
-  shows   "D"
-  using a b c d
-  by simp
-
-ML {* 
-fun procedure_inst ctxt rtrm qtrm =
-let
-  val thy = ProofContext.theory_of ctxt
-  val rtrm' = HOLogic.dest_Trueprop rtrm
-  val qtrm' = HOLogic.dest_Trueprop qtrm
-  val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
-  val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
-in
-  Drule.instantiate' [] 
-    [SOME (cterm_of thy rtrm'), 
-     SOME (cterm_of thy reg_goal),
-     SOME (cterm_of thy inj_goal)] 
-  @{thm procedure}
-end
-
-fun procedure_tac rthm =
-  Subgoal.FOCUS (fn {context, concl, ...} =>
-    let
-      val rthm' = atomize_thm rthm
-      val rule = procedure_inst context (prop_of rthm') (term_of concl)
-    in
-      EVERY1 [rtac rule, rtac rthm']
-    end)
-*}
 
 ML {*
 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"}
 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"
 *}
 
-(* FIXME: allex_prs and lambda_prs can be one function *)
-
-ML {*
-fun allex_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
-  THEN' (quotient_tac quot);
-*}
-
-ML {*
-fun lambda_prs_tac lthy quot =
-  (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}
-  THEN' (RANGE [quotient_tac quot, quotient_tac quot]));
-*}
-
-ML {*
-fun clean_tac lthy quot defs reps_same =
-  let
-    val lower = flat (map (add_lower_defs lthy) defs)
-  in
-    (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
-    (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
-    (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
-    (simp_tac (HOL_ss addsimps [reps_same]))
-  end
-*}
 
 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})

--- a/QuotMain.thy	Tue Nov 24 14:16:57 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 14:19:54 2009 +0100
@@ -1528,6 +1528,67 @@
   end
 *}
 
+lemma procedure:
+  assumes a: "A"
+  and     b: "A \<Longrightarrow> B"
+  and     c: "B = C"
+  and     d: "C = D"
+  shows   "D"
+  using a b c d
+  by simp
+
+ML {* 
+fun procedure_inst ctxt rtrm qtrm =
+let
+  val thy = ProofContext.theory_of ctxt
+  val rtrm' = HOLogic.dest_Trueprop rtrm
+  val qtrm' = HOLogic.dest_Trueprop qtrm
+  val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+  val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+in
+  Drule.instantiate' []
+    [SOME (cterm_of thy rtrm'),
+     SOME (cterm_of thy reg_goal),
+     SOME (cterm_of thy inj_goal)]
+  @{thm procedure}
+end
+
+fun procedure_tac rthm =
+  Subgoal.FOCUS (fn {context, concl, ...} =>
+    let
+      val rthm' = atomize_thm rthm
+      val rule = procedure_inst context (prop_of rthm') (term_of concl)
+    in
+      EVERY1 [rtac rule, rtac rthm']
+    end)
+*}
+
+(* FIXME: allex_prs and lambda_prs can be one function *)
+
+ML {*
+fun allex_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+  THEN' (quotient_tac quot);
+*}
+
+ML {*
+fun lambda_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}
+  THEN' (RANGE [quotient_tac quot, quotient_tac quot]));
+*}
+
+ML {*
+fun clean_tac lthy quot defs reps_same =
+  let
+    val lower = flat (map (add_lower_defs lthy) defs)
+  in
+    (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
+    (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
+    (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
+    (simp_tac (HOL_ss addsimps [reps_same]))
+  end
+*}
+
 
 end