--- a/Quot/quotient.ML	Thu Dec 10 03:48:39 2009 +0100
+++ b/Quot/quotient.ML	Thu Dec 10 04:23:13 2009 +0100
@@ -158,38 +158,11 @@
   (* FIXME: the relation needs to be a string, since its type needs *)
   (* FIXME: to recalculated in for example REGULARIZE *)
 
-  (* storing of the equiv_thm under a name *)
-  val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, 
-                           [internal_attr equiv_rules_add]) lthy3
-
-  (* interpretation *)
-  val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
-  val ((_, [eqn1pre]), lthy5) = Variable.import true [ABS_def] lthy4;
-  val eqn1i = Thm.prop_of (symmetric eqn1pre)
-  val ((_, [eqn2pre]), lthy6) = Variable.import true [REP_def] lthy5;
-  val eqn2i = Thm.prop_of (symmetric eqn2pre)
-
-  val exp_morphism = ProofContext.export_morphism lthy6 (ProofContext.init (ProofContext.theory_of lthy6));
-  val exp_term = Morphism.term exp_morphism;
-  val exp = Morphism.thm exp_morphism;
-
-  val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
-    ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
-  val mthdt = Method.Basic (fn _ => mthd)
-  val bymt = Proof.global_terminal_proof (mthdt, NONE)
-  val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
-    Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
-  lthy6
+  lthy3
   |> note (quot_thm_name, quot_thm, [])
   ||>> note (quotient_thm_name, quotient_thm, [internal_attr quotient_rules_add])
-  ||> Local_Theory.theory (fn thy =>
-      let
-        val global_eqns = map exp_term [eqn2i, eqn1i];
-        (* Not sure if the following context should not be used *)
-        val (global_eqns2, lthy7) = Variable.import_terms true global_eqns lthy6;
-        val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
-      in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
+  ||>> note (Binding.suffix_name "_equivp" qty_name, equiv_thm, [internal_attr equiv_rules_add])
 end