# HG changeset patch
# User wenzelm
# Date 1294410900 -3600
# Node ID 7f40120cd814618ae40bfec33af0b2e11444ded4
# Parent  6e93dfec9e76af79e0099c4b93b29486a4f85ec9
more precise parentheses and indentation;
eliminated trailing whitespace;

diff -r 6e93dfec9e76 -r 7f40120cd814 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Jan 07 15:35:00 2011 +0100
@@ -34,75 +34,75 @@
 
    It stores the qconst_info in the qconsts data slot.
 
-   Restriction: At the moment the left- and right-hand 
-   side of the definition must be a constant. 
+   Restriction: At the moment the left- and right-hand
+   side of the definition must be a constant.
 *)
-fun error_msg bind str = 
-let 
-  val name = Binding.name_of bind
-  val pos = Position.str_of (Binding.pos_of bind)
-in
-  error ("Head of quotient_definition " ^ 
-    quote str ^ " differs from declaration " ^ name ^ pos)
-end
+fun error_msg bind str =
+  let
+    val name = Binding.name_of bind
+    val pos = Position.str_of (Binding.pos_of bind)
+  in
+    error ("Head of quotient_definition " ^
+      quote str ^ " differs from declaration " ^ name ^ pos)
+  end
 
 fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
-let
-  val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
-  val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
-  val _ = if is_Const rhs then () else warning "The definiens is not a constant"
-  
-  fun sanity_test NONE _ = true
-    | sanity_test (SOME bind) str =
-        if Name.of_binding bind = str then true
-        else error_msg bind str
+  let
+    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
 
-  val _ = sanity_test optbind lhs_str
+    fun sanity_test NONE _ = true
+      | sanity_test (SOME bind) str =
+          if Name.of_binding bind = str then true
+          else error_msg bind str
+
+    val _ = sanity_test optbind lhs_str
 
-  val qconst_bname = Binding.name lhs_str
-  val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
-  val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
-  val (_, prop') = Local_Defs.cert_def lthy prop
-  val (_, newrhs) = Local_Defs.abs_def prop'
+    val qconst_bname = Binding.name lhs_str
+    val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
+    val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
+    val (_, prop') = Local_Defs.cert_def lthy prop
+    val (_, newrhs) = Local_Defs.abs_def prop'
 
-  val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
+    val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
 
-  (* data storage *)
-  val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+    (* data storage *)
+    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
 
-  fun qcinfo phi = transform_qconsts phi qconst_data
-  fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
-  val lthy'' = Local_Theory.declaration true
-                 (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
-in
-  (qconst_data, lthy'')
-end
+    fun qcinfo phi = transform_qconsts phi qconst_data
+    fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
+    val lthy'' = Local_Theory.declaration true
+                   (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy'
+  in
+    (qconst_data, lthy'')
+  end
 
 fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
-let
-  val lhs = Syntax.read_term lthy lhs_str
-  val rhs = Syntax.read_term lthy rhs_str
-  val lthy' = Variable.declare_term lhs lthy
-  val lthy'' = Variable.declare_term rhs lthy'
-in
-  quotient_def (decl, (attr, (lhs, rhs))) lthy''
-end
+  let
+    val lhs = Syntax.read_term lthy lhs_str
+    val rhs = Syntax.read_term lthy rhs_str
+    val lthy' = Variable.declare_term lhs lthy
+    val lthy'' = Variable.declare_term rhs lthy'
+  in
+    quotient_def (decl, (attr, (lhs, rhs))) lthy''
+  end
 
 (* a wrapper for automatically lifting a raw constant *)
 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
-let
-  val rty = fastype_of rconst
-  val qty = derive_qtyp ctxt qtys rty
-  val lhs = Free (qconst_name, qty)
-in
-  quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
-end
+  let
+    val rty = fastype_of rconst
+    val qty = derive_qtyp ctxt qtys rty
+    val lhs = Free (qconst_name, qty)
+  in
+    quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
+  end
 
 (* parser and command *)
 val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
 
 val quotdef_parser =
-  Scan.optional quotdef_decl (NONE, NoSyn) -- 
+  Scan.optional quotdef_decl (NONE, NoSyn) --
     Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
 
 val _ =
diff -r 6e93dfec9e76 -r 7f40120cd814 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Jan 07 15:35:00 2011 +0100
@@ -68,9 +68,9 @@
   Symtab.defined (MapsData.get thy) s
 
 fun maps_lookup thy s =
-  case (Symtab.lookup (MapsData.get thy) s) of
+  (case Symtab.lookup (MapsData.get thy) s of
     SOME map_fun => map_fun
-  | NONE => raise NotFound
+  | NONE => raise NotFound)
 
 fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
 fun maps_update k minfo = ProofContext.background_theory (maps_update_thy k minfo)  (* FIXME *)
@@ -80,17 +80,17 @@
 
 (* attribute to be used in declare statements *)
 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) =
-let
-  val thy = ProofContext.theory_of ctxt
-  val tyname = Sign.intern_type thy tystr
-  val mapname = Sign.intern_const thy mapstr
-  val relname = Sign.intern_const thy relstr
+  let
+    val thy = ProofContext.theory_of ctxt
+    val tyname = Sign.intern_type thy tystr
+    val mapname = Sign.intern_const thy mapstr
+    val relname = Sign.intern_const thy relstr
 
-  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
-  val _ = List.app sanity_check [mapname, relname]
-in
-  maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
-end
+    fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
+    val _ = List.app sanity_check [mapname, relname]
+  in
+    maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
+  end
 
 val maps_attr_parser =
   Args.context -- Scan.lift
@@ -103,20 +103,20 @@
     "declaration of map information"))
 
 fun print_mapsinfo ctxt =
-let
-  fun prt_map (ty_name, {mapfun, relmap}) =
-    Pretty.block (Library.separate (Pretty.brk 2)
-      (map Pretty.str
-        ["type:", ty_name,
-        "map:", mapfun,
-        "relation map:", relmap]))
-in
-  MapsData.get (ProofContext.theory_of ctxt)
-  |> Symtab.dest
-  |> map (prt_map)
-  |> Pretty.big_list "maps for type constructors:"
-  |> Pretty.writeln
-end
+  let
+    fun prt_map (ty_name, {mapfun, relmap}) =
+      Pretty.block (Library.separate (Pretty.brk 2)
+        (map Pretty.str
+          ["type:", ty_name,
+          "map:", mapfun,
+          "relation map:", relmap]))
+  in
+    MapsData.get (ProofContext.theory_of ctxt)
+    |> Symtab.dest
+    |> map (prt_map)
+    |> Pretty.big_list "maps for type constructors:"
+    |> Pretty.writeln
+  end
 
 
 (* info about quotient types *)
@@ -150,24 +150,24 @@
   map snd (Symtab.dest (QuotData.get (ProofContext.theory_of lthy)))
 
 fun print_quotinfo ctxt =
-let
-  fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
-    Pretty.block (Library.separate (Pretty.brk 2)
-     [Pretty.str "quotient type:",
-      Syntax.pretty_typ ctxt qtyp,
-      Pretty.str "raw type:",
-      Syntax.pretty_typ ctxt rtyp,
-      Pretty.str "relation:",
-      Syntax.pretty_term ctxt equiv_rel,
-      Pretty.str "equiv. thm:",
-      Syntax.pretty_term ctxt (prop_of equiv_thm)])
-in
-  QuotData.get (ProofContext.theory_of ctxt)
-  |> Symtab.dest
-  |> map (prt_quot o snd)
-  |> Pretty.big_list "quotients:"
-  |> Pretty.writeln
-end
+  let
+    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+      Pretty.block (Library.separate (Pretty.brk 2)
+       [Pretty.str "quotient type:",
+        Syntax.pretty_typ ctxt qtyp,
+        Pretty.str "raw type:",
+        Syntax.pretty_typ ctxt rtyp,
+        Pretty.str "relation:",
+        Syntax.pretty_term ctxt equiv_rel,
+        Pretty.str "equiv. thm:",
+        Syntax.pretty_term ctxt (prop_of equiv_thm)])
+  in
+    QuotData.get (ProofContext.theory_of ctxt)
+    |> Symtab.dest
+    |> map (prt_quot o snd)
+    |> Pretty.big_list "quotients:"
+    |> Pretty.writeln
+  end
 
 
 (* info about quotient constants *)
@@ -207,32 +207,32 @@
         name = name' andalso Sign.typ_instance thy (qty, qty')
       end
   in
-    case Symtab.lookup (QConstsData.get thy) name of
+    (case Symtab.lookup (QConstsData.get thy) name of
       NONE => raise NotFound
     | SOME l =>
-      (case (find_first matches l) of
-        SOME x => x
-      | NONE => raise NotFound)
+        (case find_first matches l of
+          SOME x => x
+        | NONE => raise NotFound))
   end
 
 fun print_qconstinfo ctxt =
-let
-  fun prt_qconst {qconst, rconst, def} =
-    Pretty.block (separate (Pretty.brk 1)
-     [Syntax.pretty_term ctxt qconst,
-      Pretty.str ":=",
-      Syntax.pretty_term ctxt rconst,
-      Pretty.str "as",
-      Syntax.pretty_term ctxt (prop_of def)])
-in
-  QConstsData.get (ProofContext.theory_of ctxt)
-  |> Symtab.dest
-  |> map snd
-  |> flat
-  |> map prt_qconst
-  |> Pretty.big_list "quotient constants:"
-  |> Pretty.writeln
-end
+  let
+    fun prt_qconst {qconst, rconst, def} =
+      Pretty.block (separate (Pretty.brk 1)
+       [Syntax.pretty_term ctxt qconst,
+        Pretty.str ":=",
+        Syntax.pretty_term ctxt rconst,
+        Pretty.str "as",
+        Syntax.pretty_term ctxt (prop_of def)])
+  in
+    QConstsData.get (ProofContext.theory_of ctxt)
+    |> Symtab.dest
+    |> map snd
+    |> flat
+    |> map prt_qconst
+    |> Pretty.big_list "quotient constants:"
+    |> Pretty.writeln
+  end
 
 (* equivalence relation theorems *)
 structure EquivRules = Named_Thms
diff -r 6e93dfec9e76 -r 7f40120cd814 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Jan 07 15:35:00 2011 +0100
@@ -11,10 +11,10 @@
   val injection_tac: Proof.context -> int -> tactic
   val all_injection_tac: Proof.context -> int -> tactic
   val clean_tac: Proof.context -> int -> tactic
-  
+
   val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
   val descend_tac: Proof.context -> thm list -> int -> tactic
- 
+
   val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
   val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
 
@@ -42,12 +42,12 @@
 fun OF1 thm1 thm2 = thm2 RS thm1
 
 fun atomize_thm thm =
-let
-  val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
-  val thm'' = Object_Logic.atomize (cprop_of thm')
-in
-  @{thm equal_elim_rule1} OF [thm'', thm']
-end
+  let
+    val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
+    val thm'' = Object_Logic.atomize (cprop_of thm')
+  in
+    @{thm equal_elim_rule1} OF [thm'', thm']
+  end
 
 
 
@@ -83,14 +83,14 @@
   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
 
 fun get_match_inst thy pat trm =
-let
-  val univ = Unify.matchers thy [(pat, trm)]
-  val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *)  (* FIXME fragile *)
-  val tenv = Vartab.dest (Envir.term_env env)
-  val tyenv = Vartab.dest (Envir.type_env env)
-in
-  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
-end
+  let
+    val univ = Unify.matchers thy [(pat, trm)]
+    val SOME (env, _) = Seq.pull univ           (* raises Bind, if no unifier *) (* FIXME fragile *)
+    val tenv = Vartab.dest (Envir.term_env env)
+    val tyenv = Vartab.dest (Envir.type_env env)
+  in
+    (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+  end
 
 (* Calculates the instantiations for the lemmas:
 
@@ -101,35 +101,35 @@
    theorem applies and return NONE if it doesn't.
 *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
-let
-  val thy = ProofContext.theory_of ctxt
-  fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
-  val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
-  val trm_inst = map (SOME o cterm_of thy) [R2, R1]
-in
-  case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
-    NONE => NONE
-  | SOME thm' =>
-      (case try (get_match_inst thy (get_lhs thm')) redex of
-        NONE => NONE
-      | SOME inst2 => try (Drule.instantiate inst2) thm')
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
+    val ty_inst = map (SOME o ctyp_of thy) [domain_type (fastype_of R2)]
+    val trm_inst = map (SOME o cterm_of thy) [R2, R1]
+  in
+    (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of
+      NONE => NONE
+    | SOME thm' =>
+        (case try (get_match_inst thy (get_lhs thm')) redex of
+          NONE => NONE
+        | SOME inst2 => try (Drule.instantiate inst2) thm'))
+  end
 
 fun ball_bex_range_simproc ss redex =
-let
-  val ctxt = Simplifier.the_context ss
-in
-  case redex of
-    (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
-      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
-        calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+  let
+    val ctxt = Simplifier.the_context ss
+  in
+    case redex of
+      (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
+        (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+          calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 
-  | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
-      (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
-        calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
+    | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $
+        (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
+          calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
 
-  | _ => NONE
-end
+    | _ => NONE
+  end
 
 (* Regularize works as follows:
 
@@ -159,25 +159,27 @@
 fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
 
 fun regularize_tac ctxt =
-let
-  val thy = ProofContext.theory_of ctxt
-  val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
-  val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
-  val simproc = Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
-  val simpset = (mk_minimal_ss ctxt)
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
-                       addsimprocs [simproc]
-                       addSolver equiv_solver addSolver quotient_solver
-  val eq_eqvs = eq_imp_rel_get ctxt
-in
-  simp_tac simpset THEN'
-  REPEAT_ALL_NEW (CHANGED o FIRST'
-    [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
-     resolve_tac (Inductive.get_monos ctxt),
-     resolve_tac @{thms ball_all_comm bex_ex_comm},
-     resolve_tac eq_eqvs,
-     simp_tac simpset])
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
+    val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
+    val simproc =
+      Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
+    val simpset =
+      mk_minimal_ss ctxt
+      addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+      addsimprocs [simproc]
+      addSolver equiv_solver addSolver quotient_solver
+    val eq_eqvs = eq_imp_rel_get ctxt
+  in
+    simp_tac simpset THEN'
+    REPEAT_ALL_NEW (CHANGED o FIRST'
+      [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
+       resolve_tac (Inductive.get_monos ctxt),
+       resolve_tac @{thms ball_all_comm bex_ex_comm},
+       resolve_tac eq_eqvs,
+       simp_tac simpset])
+  end
 
 
 
@@ -187,52 +189,52 @@
    is an application, it returns the function and the argument.
 *)
 fun find_qt_asm asms =
-let
-  fun find_fun trm =
-    case trm of
-      (Const(@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
-    | _ => false
-in
- case find_first find_fun asms of
-   SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
- | _ => NONE
-end
+  let
+    fun find_fun trm =
+      (case trm of
+        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Quot_True}, _) $ _)) => true
+      | _ => false)
+  in
+     (case find_first find_fun asms of
+       SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+     | _ => NONE)
+  end
 
 fun quot_true_simple_conv ctxt fnctn ctrm =
-  case (term_of ctrm) of
+  case term_of ctrm of
     (Const (@{const_name Quot_True}, _) $ x) =>
-    let
-      val fx = fnctn x;
-      val thy = ProofContext.theory_of ctxt;
-      val cx = cterm_of thy x;
-      val cfx = cterm_of thy fx;
-      val cxt = ctyp_of thy (fastype_of x);
-      val cfxt = ctyp_of thy (fastype_of fx);
-      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
-    in
-      Conv.rewr_conv thm ctrm
-    end
+      let
+        val fx = fnctn x;
+        val thy = ProofContext.theory_of ctxt;
+        val cx = cterm_of thy x;
+        val cfx = cterm_of thy fx;
+        val cxt = ctyp_of thy (fastype_of x);
+        val cfxt = ctyp_of thy (fastype_of fx);
+        val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QT_imp}
+      in
+        Conv.rewr_conv thm ctrm
+      end
 
 fun quot_true_conv ctxt fnctn ctrm =
-  case (term_of ctrm) of
+  (case term_of ctrm of
     (Const (@{const_name Quot_True}, _) $ _) =>
       quot_true_simple_conv ctxt fnctn ctrm
   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
-  | _ => Conv.all_conv ctrm
+  | _ => Conv.all_conv ctrm)
 
 fun quot_true_tac ctxt fnctn =
-   CONVERSION
+  CONVERSION
     ((Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
+        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
 
 fun dest_comb (f $ a) = (f, a)
 fun dest_bcomb ((_ $ l) $ r) = (l, r)
 
 fun unlam t =
-  case t of
-    (Abs a) => snd (Term.dest_abs a)
-  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
+  (case t of
+    Abs a => snd (Term.dest_abs a)
+  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))))
 
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 
@@ -242,53 +244,53 @@
 *)
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
-  let
-    val bare_concl = HOLogic.dest_Trueprop (term_of concl)
-    val qt_asm = find_qt_asm (map term_of asms)
-  in
-    case (bare_concl, qt_asm) of
-      (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
-         if fastype_of qt_fun = fastype_of f
-         then no_tac
-         else
-           let
-             val ty_x = fastype_of x
-             val ty_b = fastype_of qt_arg
-             val ty_f = range_type (fastype_of f)
-             val thy = ProofContext.theory_of context
-             val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
-             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
-             val inst_thm = Drule.instantiate' ty_inst
-               ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
-           in
-             (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
-           end
-    | _ => no_tac
-  end)
+    let
+      val bare_concl = HOLogic.dest_Trueprop (term_of concl)
+      val qt_asm = find_qt_asm (map term_of asms)
+    in
+      case (bare_concl, qt_asm) of
+        (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) =>
+          if fastype_of qt_fun = fastype_of f
+          then no_tac
+          else
+            let
+              val ty_x = fastype_of x
+              val ty_b = fastype_of qt_arg
+              val ty_f = range_type (fastype_of f)
+              val thy = ProofContext.theory_of context
+              val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
+              val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+              val inst_thm = Drule.instantiate' ty_inst
+                ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+            in
+              (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
+            end
+      | _ => no_tac
+    end)
 
 (* Instantiates and applies 'equals_rsp'. Since the theorem is
    complex we rely on instantiation to tell us if it applies
 *)
 fun equals_rsp_tac R ctxt =
-let
-  val thy = ProofContext.theory_of ctxt
-in
-  case try (cterm_of thy) R of (* There can be loose bounds in R *)
-    SOME ctm =>
-      let
-        val ty = domain_type (fastype_of R)
-      in
-        case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
-          [SOME (cterm_of thy R)]) @{thm equals_rsp} of
-          SOME thm => rtac thm THEN' quotient_tac ctxt
-        | NONE => K no_tac
-      end
-  | _ => K no_tac
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+  in
+    case try (cterm_of thy) R of (* There can be loose bounds in R *)
+      SOME ctm =>
+        let
+          val ty = domain_type (fastype_of R)
+        in
+          case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
+              [SOME (cterm_of thy R)]) @{thm equals_rsp} of
+            SOME thm => rtac thm THEN' quotient_tac ctxt
+          | NONE => K no_tac
+        end
+    | _ => K no_tac
+  end
 
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
-    case (try bare_concl goal) of
+    (case try bare_concl goal of
       SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
     | SOME (rel $ _ $ (rep $ (abs $ _))) =>
         let
@@ -303,7 +305,7 @@
               | NONE => no_tac)
           | NONE => no_tac
         end
-    | _ => no_tac)
+    | _ => no_tac))
 
 
 
@@ -329,67 +331,66 @@
     - reflexivity of the relation
 *)
 fun injection_match_tac ctxt = SUBGOAL (fn (goal, i) =>
-(case (bare_concl goal) of
-    (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
-  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
-      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+  (case bare_concl goal of
+      (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
+    (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
+        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
-    (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name HOL.eq},_) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
-      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+      (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
+  | (Const (@{const_name HOL.eq},_) $
+      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+        => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
 
-    (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+      (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *)
+  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+      (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
-    (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name HOL.eq},_) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+      (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
+  | Const (@{const_name HOL.eq},_) $
+      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+        => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
 
-    (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
+      (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *)
+  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+      (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+        => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
-| (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
-      => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
+  | (Const (@{const_name fun_rel}, _) $ _ $ _) $
+      (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
+        => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
 
-| (_ $
-    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
-    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
-      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+  | (_ $
+      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+      (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+        => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 
-| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
-   (rtac @{thm refl} ORELSE'
-    (equals_rsp_tac R ctxt THEN' RANGE [
-       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+  | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+     (rtac @{thm refl} ORELSE'
+      (equals_rsp_tac R ctxt THEN' RANGE [
+         quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
 
-    (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
+      (* reflexivity of operators arising from Cong_tac *)
+  | Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
 
-   (* respectfulness of constants; in particular of a simple relation *)
-| _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
-    => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
+     (* respectfulness of constants; in particular of a simple relation *)
+  | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
+      => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 
-    (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
-    (* observe map_fun *)
-| _ $ _ $ _
-    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
-       ORELSE' rep_abs_rsp_tac ctxt
+      (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
+      (* observe map_fun *)
+  | _ $ _ $ _
+      => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt)
+         ORELSE' rep_abs_rsp_tac ctxt
 
-| _ => K no_tac
-) i)
+  | _ => K no_tac) i)
 
 fun injection_step_tac ctxt rel_refl =
- FIRST' [
+  FIRST' [
     injection_match_tac ctxt,
 
     (* R (t $ ...) (t' $ ...) ----> apply_rsp   provided type of t needs lifting *)
@@ -412,11 +413,11 @@
     resolve_tac rel_refl]
 
 fun injection_tac ctxt =
-let
-  val rel_refl = reflp_get ctxt
-in
-  injection_step_tac ctxt rel_refl
-end
+  let
+    val rel_refl = reflp_get ctxt
+  in
+    injection_step_tac ctxt rel_refl
+  end
 
 fun all_injection_tac ctxt =
   REPEAT_ALL_NEW (injection_tac ctxt)
@@ -427,46 +428,48 @@
 
 (* expands all map_funs, except in front of the (bound) variables listed in xs *)
 fun map_fun_simple_conv xs ctrm =
-  case (term_of ctrm) of
+  (case term_of ctrm of
     ((Const (@{const_name "map_fun"}, _) $ _ $ _) $ h $ _) =>
         if member (op=) xs h
         then Conv.all_conv ctrm
         else Conv.rewr_conv @{thm map_fun_apply [THEN eq_reflection]} ctrm
-  | _ => Conv.all_conv ctrm
+  | _ => Conv.all_conv ctrm)
 
 fun map_fun_conv xs ctxt ctrm =
-  case (term_of ctrm) of
-      _ $ _ => (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
-                map_fun_simple_conv xs) ctrm
-    | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
-    | _ => Conv.all_conv ctrm
+  (case term_of ctrm of
+    _ $ _ =>
+      (Conv.comb_conv (map_fun_conv xs ctxt) then_conv
+        map_fun_simple_conv xs) ctrm
+  | Abs _ => Conv.abs_conv (fn (x, ctxt) => map_fun_conv ((term_of x)::xs) ctxt) ctxt ctrm
+  | _ => Conv.all_conv ctrm)
 
 fun map_fun_tac ctxt = CONVERSION (map_fun_conv [] ctxt)
 
 (* custom matching functions *)
 fun mk_abs u i t =
-  if incr_boundvars i u aconv t then Bound i else
-  case t of
-    t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
-  | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
-  | Bound j => if i = j then error "make_inst" else t
-  | _ => t
+  if incr_boundvars i u aconv t then Bound i
+  else
+    case t of
+      t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
+    | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+    | Bound j => if i = j then error "make_inst" else t
+    | _ => t
 
 fun make_inst lhs t =
-let
-  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-  val _ $ (Abs (_, _, (_ $ g))) = t;
-in
-  (f, Abs ("x", T, mk_abs u 0 g))
-end
+  let
+    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+    val _ $ (Abs (_, _, (_ $ g))) = t;
+  in
+    (f, Abs ("x", T, mk_abs u 0 g))
+  end
 
 fun make_inst_id lhs t =
-let
-  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
-  val _ $ (Abs (_, _, g)) = t;
-in
-  (f, Abs ("x", T, mk_abs u 0 g))
-end
+  let
+    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+    val _ $ (Abs (_, _, g)) = t;
+  in
+    (f, Abs ("x", T, mk_abs u 0 g))
+  end
 
 (* Simplifies a redex using the 'lambda_prs' theorem.
    First instantiates the types and known subterms.
@@ -476,7 +479,7 @@
    make_inst_id is used
 *)
 fun lambda_prs_simple_conv ctxt ctrm =
-  case (term_of ctrm) of
+  (case term_of ctrm of
     (Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
       let
         val thy = ProofContext.theory_of ctxt
@@ -495,7 +498,7 @@
       in
         Conv.rewr_conv thm4 ctrm
       end
-  | _ => Conv.all_conv ctrm
+  | _ => Conv.all_conv ctrm)
 
 fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
@@ -523,25 +526,26 @@
   4. test for refl
 *)
 fun clean_tac lthy =
-let
-  val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
-  val prs = prs_rules_get lthy
-  val ids = id_simps_get lthy
-  val thms = @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
+  let
+    val defs = map (Thm.symmetric o #def) (qconsts_dest lthy)
+    val prs = prs_rules_get lthy
+    val ids = id_simps_get lthy
+    val thms =
+      @{thms Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
 
-  val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
-in
-  EVERY' [map_fun_tac lthy,
-          lambda_prs_tac lthy,
-          simp_tac ss,
-          TRY o rtac refl]
-end
+    val ss = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+  in
+    EVERY' [map_fun_tac lthy,
+            lambda_prs_tac lthy,
+            simp_tac ss,
+            TRY o rtac refl]
+  end
 
 
 (* Tactic for Generalising Free Variables in a Goal *)
 
 fun inst_spec ctrm =
-   Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
+  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
 
 fun inst_spec_tac ctrms =
   EVERY' (map (dtac o inst_spec) ctrms)
@@ -588,31 +592,31 @@
       by (simp add: Quot_True_def)}
 
 fun lift_match_error ctxt msg rtrm qtrm =
-let
-  val rtrm_str = Syntax.string_of_term ctxt rtrm
-  val qtrm_str = Syntax.string_of_term ctxt qtrm
-  val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
-    "", "does not match with original theorem", rtrm_str]
-in
-  error msg
-end
+  let
+    val rtrm_str = Syntax.string_of_term ctxt rtrm
+    val qtrm_str = Syntax.string_of_term ctxt qtrm
+    val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str,
+      "", "does not match with original theorem", rtrm_str]
+  in
+    error msg
+  end
 
 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 = regularize_trm_chk ctxt (rtrm', qtrm')
-    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
-  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
-    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
-in
-  Drule.instantiate' []
-    [SOME (cterm_of thy rtrm'),
-     SOME (cterm_of thy reg_goal),
-     NONE,
-     SOME (cterm_of thy inj_goal)] lifting_procedure_thm
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val rtrm' = HOLogic.dest_Trueprop rtrm
+    val qtrm' = HOLogic.dest_Trueprop qtrm
+    val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
+      handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+    val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
+      handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
+  in
+    Drule.instantiate' []
+      [SOME (cterm_of thy rtrm'),
+       SOME (cterm_of thy reg_goal),
+       NONE,
+       SOME (cterm_of thy inj_goal)] lifting_procedure_thm
+  end
 
 
 (* Since we use Ball and Bex during the lifting and descending,
@@ -625,34 +629,34 @@
 (** descending as tactic **)
 
 fun descend_procedure_tac ctxt simps =
-let
-  val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
-in
-  full_simp_tac ss
-  THEN' Object_Logic.full_atomize_tac
-  THEN' gen_frees_tac ctxt
-  THEN' SUBGOAL (fn (goal, i) =>
-        let
-          val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
-          val rtrm = derive_rtrm ctxt qtys goal
-          val rule = procedure_inst ctxt rtrm  goal
-        in
-          rtac rule i
-        end)
-end
+  let
+    val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+  in
+    full_simp_tac ss
+    THEN' Object_Logic.full_atomize_tac
+    THEN' gen_frees_tac ctxt
+    THEN' SUBGOAL (fn (goal, i) =>
+      let
+        val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+        val rtrm = derive_rtrm ctxt qtys goal
+        val rule = procedure_inst ctxt rtrm  goal
+      in
+        rtac rule i
+      end)
+  end
 
 fun descend_tac ctxt simps =
-let
-  val mk_tac_raw =
-    descend_procedure_tac ctxt simps
-    THEN' RANGE
-      [Object_Logic.rulify_tac THEN' (K all_tac),
-       regularize_tac ctxt,
-       all_injection_tac ctxt,
-       clean_tac ctxt]
-in
-  Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
-end
+  let
+    val mk_tac_raw =
+      descend_procedure_tac ctxt simps
+      THEN' RANGE
+        [Object_Logic.rulify_tac THEN' (K all_tac),
+         regularize_tac ctxt,
+         all_injection_tac ctxt,
+         clean_tac ctxt]
+  in
+    Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
+  end
 
 
 (** lifting as a tactic **)
@@ -660,29 +664,29 @@
 
 (* the tactic leaves three subgoals to be proved *)
 fun lift_procedure_tac ctxt simps rthm =
-let
-  val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
-in
-  full_simp_tac ss
-  THEN' Object_Logic.full_atomize_tac
-  THEN' gen_frees_tac ctxt
-  THEN' SUBGOAL (fn (goal, i) =>
-    let
-      (* full_atomize_tac contracts eta redexes,
-         so we do it also in the original theorem *)
-      val rthm' = 
-        rthm |> full_simplify ss
-             |> Drule.eta_contraction_rule 
-             |> Thm.forall_intr_frees
-             |> atomize_thm 
+  let
+    val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
+  in
+    full_simp_tac ss
+    THEN' Object_Logic.full_atomize_tac
+    THEN' gen_frees_tac ctxt
+    THEN' SUBGOAL (fn (goal, i) =>
+      let
+        (* full_atomize_tac contracts eta redexes,
+           so we do it also in the original theorem *)
+        val rthm' =
+          rthm |> full_simplify ss
+               |> Drule.eta_contraction_rule
+               |> Thm.forall_intr_frees
+               |> atomize_thm
 
-      val rule = procedure_inst ctxt (prop_of rthm') goal
-    in
-      (rtac rule THEN' rtac rthm') i
-    end)
-end
+        val rule = procedure_inst ctxt (prop_of rthm') goal
+      in
+        (rtac rule THEN' rtac rthm') i
+      end)
+  end
 
-fun lift_single_tac ctxt simps rthm = 
+fun lift_single_tac ctxt simps rthm =
   lift_procedure_tac ctxt simps rthm
   THEN' RANGE
     [ regularize_tac ctxt,
@@ -690,26 +694,26 @@
       clean_tac ctxt ]
 
 fun lift_tac ctxt simps rthms =
-  Goal.conjunction_tac 
+  Goal.conjunction_tac
   THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
 
 
 (* automated lifting with pre-simplification of the theorems;
    for internal usage *)
 fun lifted ctxt qtys simps rthm =
-let
-  val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
-  val goal = derive_qtrm ctxt' qtys (prop_of rthm')
-in
-  Goal.prove ctxt' [] [] goal 
-    (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
-  |> singleton (ProofContext.export ctxt' ctxt)
-end
+  let
+    val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
+    val goal = derive_qtrm ctxt' qtys (prop_of rthm')
+  in
+    Goal.prove ctxt' [] [] goal
+      (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
+    |> singleton (ProofContext.export ctxt' ctxt)
+  end
 
 
 (* lifting as an attribute *)
 
-val lifted_attrib = Thm.rule_attribute (fn context => 
+val lifted_attrib = Thm.rule_attribute (fn context =>
   let
     val ctxt = Context.proof_of context
     val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
diff -r 6e93dfec9e76 -r 7f40120cd814 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Jan 07 15:35:00 2011 +0100
@@ -65,13 +65,13 @@
   | RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1
 
 fun get_mapfun ctxt s =
-let
-  val thy = ProofContext.theory_of ctxt
-  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
-    raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
-in
-  Const (mapfun, dummyT)
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
+      raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+  in
+    Const (mapfun, dummyT)
+  end
 
 (* makes a Free out of a TVar *)
 fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
@@ -85,74 +85,74 @@
    it produces:     %a b. prod_map (map a) b
 *)
 fun mk_mapfun ctxt vs rty =
-let
-  val vs' = map mk_Free vs
+  let
+    val vs' = map mk_Free vs
 
-  fun mk_mapfun_aux rty =
-    case rty of
-      TVar _ => mk_Free rty
-    | Type (_, []) => mk_identity rty
-    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
-    | _ => raise LIFT_MATCH "mk_mapfun (default)"
-in
-  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
-end
+    fun mk_mapfun_aux rty =
+      case rty of
+        TVar _ => mk_Free rty
+      | Type (_, []) => mk_identity rty
+      | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
+      | _ => raise LIFT_MATCH "mk_mapfun (default)"
+  in
+    fold_rev Term.lambda vs' (mk_mapfun_aux rty)
+  end
 
 (* looks up the (varified) rty and qty for
    a quotient definition
 *)
 fun get_rty_qty ctxt s =
-let
-  val thy = ProofContext.theory_of ctxt
-  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
-    raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
-in
-  (#rtyp qdata, #qtyp qdata)
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
+      raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+  in
+    (#rtyp qdata, #qtyp qdata)
+  end
 
 (* takes two type-environments and looks
    up in both of them the variable v, which
    must be listed in the environment
 *)
 fun double_lookup rtyenv qtyenv v =
-let
-  val v' = fst (dest_TVar v)
-in
-  (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
-end
+  let
+    val v' = fst (dest_TVar v)
+  in
+    (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+  end
 
 (* matches a type pattern with a type *)
 fun match ctxt err ty_pat ty =
-let
-  val thy = ProofContext.theory_of ctxt
-in
-  Sign.typ_match thy (ty_pat, ty) Vartab.empty
-  handle Type.TYPE_MATCH => err ctxt ty_pat ty
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+  in
+    Sign.typ_match thy (ty_pat, ty) Vartab.empty
+      handle Type.TYPE_MATCH => err ctxt ty_pat ty
+  end
 
 (* produces the rep or abs constant for a qty *)
 fun absrep_const flag ctxt qty_str =
-let
-  val qty_name = Long_Name.base_name qty_str
-  val qualifier = Long_Name.qualifier qty_str
-in
-  case flag of
-    AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
-  | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
-end
+  let
+    val qty_name = Long_Name.base_name qty_str
+    val qualifier = Long_Name.qualifier qty_str
+  in
+    case flag of
+      AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
+    | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+  end
 
 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
 fun absrep_const_chk flag ctxt qty_str =
   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
 
 fun absrep_match_err ctxt ty_pat ty =
-let
-  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
-  val ty_str = Syntax.string_of_typ ctxt ty
-in
-  raise LIFT_MATCH (space_implode " "
-    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
-end
+  let
+    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+    val ty_str = Syntax.string_of_typ ctxt ty
+  in
+    raise LIFT_MATCH (space_implode " "
+      ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+  end
 
 
 (** generation of an aggregate absrep function **)
@@ -213,29 +213,29 @@
     | (Type (s, tys), Type (s', tys')) =>
         if s = s'
         then
-           let
-             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
-           in
-             list_comb (get_mapfun ctxt s, args)
-           end
+          let
+            val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+          in
+            list_comb (get_mapfun ctxt s, args)
+          end
         else
-           let
-             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-             val rtyenv = match ctxt absrep_match_err rty_pat rty
-             val qtyenv = match ctxt absrep_match_err qty_pat qty
-             val args_aux = map (double_lookup rtyenv qtyenv) vs
-             val args = map (absrep_fun flag ctxt) args_aux
-           in
-             if forall is_identity args
-             then absrep_const flag ctxt s'
-             else 
-               let
-                 val map_fun = mk_mapfun ctxt vs rty_pat
-                 val result = list_comb (map_fun, args)
-               in
-                 mk_fun_compose flag (absrep_const flag ctxt s', result)
-               end
-           end
+          let
+            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+            val rtyenv = match ctxt absrep_match_err rty_pat rty
+            val qtyenv = match ctxt absrep_match_err qty_pat qty
+            val args_aux = map (double_lookup rtyenv qtyenv) vs
+            val args = map (absrep_fun flag ctxt) args_aux
+          in
+            if forall is_identity args
+            then absrep_const flag ctxt s'
+            else
+              let
+                val map_fun = mk_mapfun ctxt vs rty_pat
+                val result = list_comb (map_fun, args)
+              in
+                mk_fun_compose flag (absrep_const flag ctxt s', result)
+              end
+          end
     | (TFree x, TFree x') =>
         if x = x'
         then mk_identity rty
@@ -259,13 +259,13 @@
 
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
-let
-  val thy = ProofContext.theory_of ctxt
-  val trm_ty = fastype_of trm
-  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
-in
-  map_types (Envir.subst_type ty_inst) trm
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val trm_ty = fastype_of trm
+    val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
+  in
+    map_types (Envir.subst_type ty_inst) trm
+  end
 
 fun is_eq (Const (@{const_name HOL.eq}, _)) = true
   | is_eq _ = false
@@ -274,44 +274,44 @@
   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
 fun get_relmap ctxt s =
-let
-  val thy = ProofContext.theory_of ctxt
-  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
-    raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
-in
-  Const (relmap, dummyT)
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+    val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
+      raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+  in
+    Const (relmap, dummyT)
+  end
 
 fun mk_relmap ctxt vs rty =
-let
-  val vs' = map (mk_Free) vs
+  let
+    val vs' = map (mk_Free) vs
 
-  fun mk_relmap_aux rty =
-    case rty of
-      TVar _ => mk_Free rty
-    | Type (_, []) => HOLogic.eq_const rty
-    | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
-    | _ => raise LIFT_MATCH ("mk_relmap (default)")
-in
-  fold_rev Term.lambda vs' (mk_relmap_aux rty)
-end
+    fun mk_relmap_aux rty =
+      case rty of
+        TVar _ => mk_Free rty
+      | Type (_, []) => HOLogic.eq_const rty
+      | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
+      | _ => raise LIFT_MATCH ("mk_relmap (default)")
+  in
+    fold_rev Term.lambda vs' (mk_relmap_aux rty)
+  end
 
 fun get_equiv_rel ctxt s =
-let
-  val thy = ProofContext.theory_of ctxt
-in
-  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
-    raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+  in
+    #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
+      raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+  end
 
 fun equiv_match_err ctxt ty_pat ty =
-let
-  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
-  val ty_str = Syntax.string_of_typ ctxt ty
-in
-  raise LIFT_MATCH (space_implode " "
-    ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
-end
+  let
+    val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+    val ty_str = Syntax.string_of_typ ctxt ty
+  in
+    raise LIFT_MATCH (space_implode " "
+      ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+  end
 
 (* builds the aggregate equivalence relation
    that will be the argument of Respects
@@ -322,34 +322,34 @@
   else
     case (rty, qty) of
       (Type (s, tys), Type (s', tys')) =>
-       if s = s'
-       then
-         let
-           val args = map (equiv_relation ctxt) (tys ~~ tys')
-         in
-           list_comb (get_relmap ctxt s, args)
-         end
-       else
-         let
-           val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
-           val rtyenv = match ctxt equiv_match_err rty_pat rty
-           val qtyenv = match ctxt equiv_match_err qty_pat qty
-           val args_aux = map (double_lookup rtyenv qtyenv) vs
-           val args = map (equiv_relation ctxt) args_aux
-           val eqv_rel = get_equiv_rel ctxt s'
-           val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
-         in
-           if forall is_eq args
-           then eqv_rel'
-           else 
-             let 
-               val rel_map = mk_relmap ctxt vs rty_pat
-               val result = list_comb (rel_map, args)
-             in
-               mk_rel_compose (result, eqv_rel')
-             end
-         end
-      | _ => HOLogic.eq_const rty
+        if s = s'
+        then
+          let
+            val args = map (equiv_relation ctxt) (tys ~~ tys')
+          in
+            list_comb (get_relmap ctxt s, args)
+          end
+        else
+          let
+            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+            val rtyenv = match ctxt equiv_match_err rty_pat rty
+            val qtyenv = match ctxt equiv_match_err qty_pat qty
+            val args_aux = map (double_lookup rtyenv qtyenv) vs
+            val args = map (equiv_relation ctxt) args_aux
+            val eqv_rel = get_equiv_rel ctxt s'
+            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
+          in
+            if forall is_eq args
+            then eqv_rel'
+            else
+              let
+                val rel_map = mk_relmap ctxt vs rty_pat
+                val result = list_comb (rel_map, args)
+              in
+                mk_rel_compose (result, eqv_rel')
+              end
+          end
+    | _ => HOLogic.eq_const rty
 
 fun equiv_relation_chk ctxt (rty, qty) =
   equiv_relation ctxt (rty, qty)
@@ -414,14 +414,14 @@
   | _ => f (trm1, trm2)
 
 fun term_mismatch str ctxt t1 t2 =
-let
-  val t1_str = Syntax.string_of_term ctxt t1
-  val t2_str = Syntax.string_of_term ctxt t2
-  val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
-  val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
-in
-  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
-end
+  let
+    val t1_str = Syntax.string_of_term ctxt t1
+    val t2_str = Syntax.string_of_term ctxt t2
+    val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
+    val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
+  in
+    raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
+  end
 
 (* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)
@@ -429,17 +429,18 @@
 (* Checks that two types match, for example:
      rty -> rty   matches   qty -> qty *)
 fun matches_typ thy rT qT =
-  if rT = qT then true else
-  case (rT, qT) of
-    (Type (rs, rtys), Type (qs, qtys)) =>
-      if rs = qs then
-        if length rtys <> length qtys then false else
-        forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
-      else
-        (case quotdata_lookup_raw thy qs of
-          SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
-        | NONE => false)
-  | _ => false
+  if rT = qT then true
+  else
+    (case (rT, qT) of
+      (Type (rs, rtys), Type (qs, qtys)) =>
+        if rs = qs then
+          if length rtys <> length qtys then false
+          else forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
+        else
+          (case quotdata_lookup_raw thy qs of
+            SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+          | NONE => false)
+    | _ => false)
 
 
 (* produces a regularized version of rtrm
@@ -452,124 +453,124 @@
 fun regularize_trm ctxt (rtrm, qtrm) =
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (_, ty', t')) =>
-       let
-         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
-       in
-         if ty = ty' then subtrm
-         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
-       end
+      let
+        val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
+      in
+        if ty = ty' then subtrm
+        else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
+      end
   | (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
-       let
-         val subtrm = regularize_trm ctxt (t, t')
-         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
-       in
-         if resrel <> needres
-         then term_mismatch "regularize (Babs)" ctxt resrel needres
-         else mk_babs $ resrel $ subtrm
-       end
+      let
+        val subtrm = regularize_trm ctxt (t, t')
+        val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
+      in
+        if resrel <> needres
+        then term_mismatch "regularize (Babs)" ctxt resrel needres
+        else mk_babs $ resrel $ subtrm
+      end
 
   | (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-       in
-         if ty = ty' then Const (@{const_name All}, ty) $ subtrm
-         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
+      let
+        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+      in
+        if ty = ty' then Const (@{const_name All}, ty) $ subtrm
+        else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+      end
 
   | (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-       in
-         if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
-         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
+      let
+        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+      in
+        if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
+        else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+      end
 
   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
       (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
      Const (@{const_name Ex1}, ty') $ t') =>
-       let
-         val t_ = incr_boundvars (~1) t
-         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
-         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-       in
-         if resrel <> needrel
-         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
-         else mk_bex1_rel $ resrel $ subtrm
-       end
+      let
+        val t_ = incr_boundvars (~1) t
+        val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
+        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+      in
+        if resrel <> needrel
+        then term_mismatch "regularize (Bex1)" ctxt resrel needrel
+        else mk_bex1_rel $ resrel $ subtrm
+      end
 
   | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-       in
-         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
-         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
-       end
+      let
+        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+      in
+        if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
+        else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+      end
 
   | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
      Const (@{const_name All}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-       in
-         if resrel <> needrel
-         then term_mismatch "regularize (Ball)" ctxt resrel needrel
-         else mk_ball $ (mk_resp $ resrel) $ subtrm
-       end
+      let
+        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+      in
+        if resrel <> needrel
+        then term_mismatch "regularize (Ball)" ctxt resrel needrel
+        else mk_ball $ (mk_resp $ resrel) $ subtrm
+      end
 
   | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
      Const (@{const_name Ex}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-       in
-         if resrel <> needrel
-         then term_mismatch "regularize (Bex)" ctxt resrel needrel
-         else mk_bex $ (mk_resp $ resrel) $ subtrm
-       end
+      let
+        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+      in
+        if resrel <> needrel
+        then term_mismatch "regularize (Bex)" ctxt resrel needrel
+        else mk_bex $ (mk_resp $ resrel) $ subtrm
+      end
 
   | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
-       let
-         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
-       in
-         if resrel <> needrel
-         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
-         else mk_bex1_rel $ resrel $ subtrm
-       end
+      let
+        val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+        val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
+      in
+        if resrel <> needrel
+        then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
+        else mk_bex1_rel $ resrel $ subtrm
+      end
 
   | (* equalities need to be replaced by appropriate equivalence relations *)
     (Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) =>
-         if ty = ty' then rtrm
-         else equiv_relation ctxt (domain_type ty, domain_type ty')
+        if ty = ty' then rtrm
+        else equiv_relation ctxt (domain_type ty, domain_type ty')
 
   | (* in this case we just check whether the given equivalence relation is correct *)
     (rel, Const (@{const_name HOL.eq}, ty')) =>
-       let
-         val rel_ty = fastype_of rel
-         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
-       in
-         if rel' aconv rel then rtrm
-         else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
-       end
+      let
+        val rel_ty = fastype_of rel
+        val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
+      in
+        if rel' aconv rel then rtrm
+        else term_mismatch "regularize (relation mismatch)" ctxt rel rel'
+      end
 
   | (_, Const _) =>
-       let
-         val thy = ProofContext.theory_of ctxt
-         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
-           | same_const _ _ = false
-       in
-         if same_const rtrm qtrm then rtrm
-         else
-           let
-             val rtrm' = #rconst (qconsts_lookup thy qtrm)
-               handle Quotient_Info.NotFound =>
+      let
+        val thy = ProofContext.theory_of ctxt
+        fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
+          | same_const _ _ = false
+      in
+        if same_const rtrm qtrm then rtrm
+        else
+          let
+            val rtrm' = #rconst (qconsts_lookup thy qtrm)
+              handle Quotient_Info.NotFound =>
                 term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
-           in
-             if Pattern.matches thy (rtrm', rtrm)
-             then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
-           end
-       end
+          in
+            if Pattern.matches thy (rtrm', rtrm)
+            then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
+          end
+      end
 
   | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
      ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
@@ -583,16 +584,16 @@
        regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
 
   | (Bound i, Bound i') =>
-       if i = i' then rtrm
-       else raise (LIFT_MATCH "regularize (bounds mismatch)")
+      if i = i' then rtrm
+      else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
   | _ =>
-       let
-         val rtrm_str = Syntax.string_of_term ctxt rtrm
-         val qtrm_str = Syntax.string_of_term ctxt qtrm
-       in
-         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
-       end
+      let
+        val rtrm_str = Syntax.string_of_term ctxt rtrm
+        val qtrm_str = Syntax.string_of_term ctxt qtrm
+      in
+        raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
+      end
 
 fun regularize_trm_chk ctxt (rtrm, qtrm) =
   regularize_trm ctxt (rtrm, qtrm)
@@ -635,12 +636,12 @@
   absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
 
 fun inj_repabs_err ctxt msg rtrm qtrm =
-let
-  val rtrm_str = Syntax.string_of_term ctxt rtrm
-  val qtrm_str = Syntax.string_of_term ctxt qtrm
-in
-  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
-end
+  let
+    val rtrm_str = Syntax.string_of_term ctxt rtrm
+    val qtrm_str = Syntax.string_of_term ctxt qtrm
+  in
+    raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+  end
 
 
 (* bound variables need to be treated properly,
@@ -717,8 +718,8 @@
                 NONE => matches tail
               | SOME inst => Envir.subst_type inst qty
       in
-        matches ty_subst 
-      end 
+        matches ty_subst
+      end
   | _ => rty
 
 fun subst_trm ctxt ty_subst trm_subst rtrm =
@@ -728,7 +729,7 @@
   | Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty)
   | Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty)
   | Bound i => Bound i
-  | Const (a, ty) => 
+  | Const (a, ty) =>
       let
         val thy = ProofContext.theory_of ctxt
 
@@ -742,43 +743,43 @@
       end
 
 (* generate type and term substitutions out of the
-   qtypes involved in a quotient; the direction flag 
-   indicates in which direction the substitutions work: 
-   
+   qtypes involved in a quotient; the direction flag
+   indicates in which direction the substitutions work:
+
      true:  quotient -> raw
      false: raw -> quotient
 *)
 fun mk_ty_subst qtys direction ctxt =
-let
-  val thy = ProofContext.theory_of ctxt  
-in
-  quotdata_dest ctxt
-   |> map (fn x => (#rtyp x, #qtyp x))
-   |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
-   |> map (if direction then swap else I)
-end
+  let
+    val thy = ProofContext.theory_of ctxt
+  in
+    quotdata_dest ctxt
+    |> map (fn x => (#rtyp x, #qtyp x))
+    |> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty)
+    |> map (if direction then swap else I)
+  end
 
 fun mk_trm_subst qtys direction ctxt =
-let
-  val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
-  fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
+  let
+    val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt)
+    fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2
 
-  val const_substs = 
-    qconsts_dest ctxt
-     |> map (fn x => (#rconst x, #qconst x))
-     |> map (if direction then swap else I)
+    val const_substs =
+      qconsts_dest ctxt
+      |> map (fn x => (#rconst x, #qconst x))
+      |> map (if direction then swap else I)
 
-  val rel_substs =
-    quotdata_dest ctxt
-     |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
-     |> map (if direction then swap else I)
-in
-  filter proper (const_substs @ rel_substs)
-end
+    val rel_substs =
+      quotdata_dest ctxt
+      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+      |> map (if direction then swap else I)
+  in
+    filter proper (const_substs @ rel_substs)
+  end
 
 
 (* derives a qtyp and qtrm out of a rtyp and rtrm,
-   respectively 
+   respectively
 *)
 fun derive_qtyp ctxt qtys rty =
   subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
@@ -787,7 +788,7 @@
   subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
 
 (* derives a rtyp and rtrm out of a qtyp and qtrm,
-   respectively 
+   respectively
 *)
 fun derive_rtyp ctxt qtys qty =
   subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
diff -r 6e93dfec9e76 -r 7f40120cd814 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Jan 07 14:58:15 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Jan 07 15:35:00 2011 +0100
@@ -24,12 +24,12 @@
 
 (* wrappers for define, note, Attrib.internal and theorem_i *)
 fun define (name, mx, rhs) lthy =
-let
-  val ((rhs, (_ , thm)), lthy') =
-     Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
-in
-  ((rhs, thm), lthy')
-end
+  let
+    val ((rhs, (_ , thm)), lthy') =
+      Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
+  in
+    ((rhs, thm), lthy')
+  end
 
 fun note (name, thm, attrs) lthy =
   Local_Theory.note ((name, attrs), [thm]) lthy |> snd
@@ -38,12 +38,12 @@
 fun intern_attr at = Attrib.internal (K at)
 
 fun theorem after_qed goals ctxt =
-let
-  val goals' = map (rpair []) goals
-  fun after_qed' thms = after_qed (the_single thms)
-in
-  Proof.theorem NONE after_qed' [goals'] ctxt
-end
+  let
+    val goals' = map (rpair []) goals
+    fun after_qed' thms = after_qed (the_single thms)
+  in
+    Proof.theorem NONE after_qed' [goals'] ctxt
+  end
 
 
 
@@ -54,178 +54,179 @@
 
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
 fun typedef_term rel rty lthy =
-let
-  val [x, c] =
-    [("x", rty), ("c", HOLogic.mk_setT rty)]
-    |> Variable.variant_frees lthy [rel]
-    |> map Free
-in
-  lambda c (HOLogic.exists_const rty $
-     lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
-end
+  let
+    val [x, c] =
+      [("x", rty), ("c", HOLogic.mk_setT rty)]
+      |> Variable.variant_frees lthy [rel]
+      |> map Free
+  in
+    lambda c (HOLogic.exists_const rty $
+        lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
+  end
 
 
 (* makes the new type definitions and proves non-emptyness *)
 fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
-let
-  val typedef_tac =
-    EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
-in
-(* FIXME: purely local typedef causes at the moment 
-   problems with type variables
-  
-  Typedef.add_typedef false NONE (qty_name, vs, mx) 
-    (typedef_term rel rty lthy) NONE typedef_tac lthy
-*)
-(* FIXME should really use local typedef here *)
-   Local_Theory.background_theory_result
+  let
+    val typedef_tac =
+      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
+  in
+  (* FIXME: purely local typedef causes at the moment
+     problems with type variables
+
+    Typedef.add_typedef false NONE (qty_name, vs, mx)
+      (typedef_term rel rty lthy) NONE typedef_tac lthy
+  *)
+  (* FIXME should really use local typedef here *)
+    Local_Theory.background_theory_result
      (Typedef.add_typedef_global false NONE
        (qty_name, map (rpair dummyS) vs, mx)
          (typedef_term rel rty lthy)
            NONE typedef_tac) lthy
-end
+  end
 
 
 (* tactic to prove the quot_type theorem for the new type *)
 fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
-let
-  val rep_thm = #Rep typedef_info RS mem_def1
-  val rep_inv = #Rep_inverse typedef_info
-  val abs_inv = #Abs_inverse typedef_info
-  val rep_inj = #Rep_inject typedef_info
-in
-  (rtac @{thm quot_type.intro} THEN' RANGE [
-    rtac equiv_thm,
-    rtac rep_thm,
-    rtac rep_inv,
-    rtac abs_inv THEN' rtac mem_def2 THEN' atac,
-    rtac rep_inj]) 1
-end
+  let
+    val rep_thm = #Rep typedef_info RS mem_def1
+    val rep_inv = #Rep_inverse typedef_info
+    val abs_inv = #Abs_inverse typedef_info
+    val rep_inj = #Rep_inject typedef_info
+  in
+    (rtac @{thm quot_type.intro} THEN' RANGE [
+      rtac equiv_thm,
+      rtac rep_thm,
+      rtac rep_inv,
+      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
+      rtac rep_inj]) 1
+  end
 
 (* proves the quot_type theorem for the new type *)
 fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
-let
-  val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
-  val goal =
-    HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
-    |> Syntax.check_term lthy
-in
-  Goal.prove lthy [] [] goal
-    (K (typedef_quot_type_tac equiv_thm typedef_info))
-end
+  let
+    val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
+    val goal =
+      HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
+      |> Syntax.check_term lthy
+  in
+    Goal.prove lthy [] [] goal
+      (K (typedef_quot_type_tac equiv_thm typedef_info))
+  end
 
 (* main function for constructing a quotient type *)
 fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
-let
-  val part_equiv = 
-    if partial 
-    then equiv_thm 
-    else equiv_thm RS @{thm equivp_implies_part_equivp}
+  let
+    val part_equiv =
+      if partial
+      then equiv_thm
+      else equiv_thm RS @{thm equivp_implies_part_equivp}
 
-  (* generates the typedef *)
-  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
+    (* generates the typedef *)
+    val ((qty_full_name, typedef_info), lthy1) =
+      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
 
-  (* abs and rep functions from the typedef *)
-  val Abs_ty = #abs_type (#1 typedef_info)
-  val Rep_ty = #rep_type (#1 typedef_info)
-  val Abs_name = #Abs_name (#1 typedef_info)
-  val Rep_name = #Rep_name (#1 typedef_info)
-  val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
-  val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
+    (* abs and rep functions from the typedef *)
+    val Abs_ty = #abs_type (#1 typedef_info)
+    val Rep_ty = #rep_type (#1 typedef_info)
+    val Abs_name = #Abs_name (#1 typedef_info)
+    val Rep_name = #Rep_name (#1 typedef_info)
+    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
+    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
 
-  (* more useful abs and rep definitions *)
-  val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
-  val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
-  val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
-  val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
-  val abs_name = Binding.prefix_name "abs_" qty_name
-  val rep_name = Binding.prefix_name "rep_" qty_name
+    (* more useful abs and rep definitions *)
+    val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
+    val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
+    val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
+    val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
+    val abs_name = Binding.prefix_name "abs_" qty_name
+    val rep_name = Binding.prefix_name "rep_" qty_name
 
-  val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
-  val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
+    val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
+    val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
 
-  (* quot_type theorem *)
-  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
+    (* quot_type theorem *)
+    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
 
-  (* quotient theorem *)
-  val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
-  val quotient_thm = 
-    (quot_thm RS @{thm quot_type.Quotient})
-    |> fold_rule [abs_def, rep_def]
+    (* quotient theorem *)
+    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
+    val quotient_thm =
+      (quot_thm RS @{thm quot_type.Quotient})
+      |> fold_rule [abs_def, rep_def]
 
-  (* name equivalence theorem *)
-  val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
+    (* name equivalence theorem *)
+    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 
-  (* storing the quotdata *)
-  val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
+    (* storing the quotdata *)
+    val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
 
-  fun qinfo phi = transform_quotdata phi quotdata
+    fun qinfo phi = transform_quotdata phi quotdata
 
-  val lthy4 = lthy3
-     |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
-     |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
-     |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
-in
-  (quotdata, lthy4)
-end
+    val lthy4 = lthy3
+      |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
+      |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
+      |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
+  in
+    (quotdata, lthy4)
+  end
 
 
 (* sanity checks for the quotient type specifications *)
 fun sanity_check ((vs, qty_name, _), (rty, rel, _)) =
-let
-  val rty_tfreesT = map fst (Term.add_tfreesT rty [])
-  val rel_tfrees = map fst (Term.add_tfrees rel [])
-  val rel_frees = map fst (Term.add_frees rel [])
-  val rel_vars = Term.add_vars rel []
-  val rel_tvars = Term.add_tvars rel []
-  val qty_str = Binding.str_of qty_name ^ ": "
+  let
+    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
+    val rel_tfrees = map fst (Term.add_tfrees rel [])
+    val rel_frees = map fst (Term.add_frees rel [])
+    val rel_vars = Term.add_vars rel []
+    val rel_tvars = Term.add_tvars rel []
+    val qty_str = Binding.str_of qty_name ^ ": "
 
-  val illegal_rel_vars =
-    if null rel_vars andalso null rel_tvars then []
-    else [qty_str ^ "illegal schematic variable(s) in the relation."]
+    val illegal_rel_vars =
+      if null rel_vars andalso null rel_tvars then []
+      else [qty_str ^ "illegal schematic variable(s) in the relation."]
 
-  val dup_vs =
-    (case duplicates (op =) vs of
-       [] => []
-     | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
+    val dup_vs =
+      (case duplicates (op =) vs of
+        [] => []
+      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
 
-  val extra_rty_tfrees =
-    (case subtract (op =) vs rty_tfreesT of
-       [] => []
-     | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
+    val extra_rty_tfrees =
+      (case subtract (op =) vs rty_tfreesT of
+        [] => []
+      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
 
-  val extra_rel_tfrees =
-    (case subtract (op =) vs rel_tfrees of
-       [] => []
-     | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
+    val extra_rel_tfrees =
+      (case subtract (op =) vs rel_tfrees of
+        [] => []
+      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
 
-  val illegal_rel_frees =
-    (case rel_frees of
-      [] => []
-    | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
+    val illegal_rel_frees =
+      (case rel_frees of
+        [] => []
+      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
 
-  val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
-in
-  if null errs then () else error (cat_lines errs)
-end
+    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
+  in
+    if null errs then () else error (cat_lines errs)
+  end
 
 (* check for existence of map functions *)
 fun map_check ctxt (_, (rty, _, _)) =
-let
-  val thy = ProofContext.theory_of ctxt
+  let
+    val thy = ProofContext.theory_of ctxt
 
-  fun map_check_aux rty warns =
-    case rty of
-      Type (_, []) => warns
-    | Type (s, _) => if maps_defined thy s then warns else s::warns
-    | _ => warns
+    fun map_check_aux rty warns =
+      case rty of
+        Type (_, []) => warns
+      | Type (s, _) => if maps_defined thy s then warns else s::warns
+      | _ => warns
 
-  val warns = map_check_aux rty []
-in
-  if null warns then ()
-  else warning ("No map function defined for " ^ commas warns ^
-    ". This will cause problems later on.")
-end
+    val warns = map_check_aux rty []
+  in
+    if null warns then ()
+    else warning ("No map function defined for " ^ commas warns ^
+      ". This will cause problems later on.")
+  end
 
 
 
@@ -246,48 +247,48 @@
 *)
 
 fun quotient_type quot_list lthy =
-let
-  (* sanity check *)
-  val _ = List.app sanity_check quot_list
-  val _ = List.app (map_check lthy) quot_list
+  let
+    (* sanity check *)
+    val _ = List.app sanity_check quot_list
+    val _ = List.app (map_check lthy) quot_list
 
-  fun mk_goal (rty, rel, partial) =
-  let
-    val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
-    val const = 
-      if partial then @{const_name part_equivp} else @{const_name equivp}
+    fun mk_goal (rty, rel, partial) =
+      let
+        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+        val const =
+          if partial then @{const_name part_equivp} else @{const_name equivp}
+      in
+        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
+      end
+
+    val goals = map (mk_goal o snd) quot_list
+
+    fun after_qed thms lthy =
+      fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
   in
-    HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
+    theorem after_qed goals lthy
   end
 
-  val goals = map (mk_goal o snd) quot_list
-
-  fun after_qed thms lthy =
-    fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
-in
-  theorem after_qed goals lthy
-end
-
 fun quotient_type_cmd specs lthy =
-let
-  fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
   let
-    val rty = Syntax.read_typ lthy rty_str
-    val lthy1 = Variable.declare_typ rty lthy
-    val rel = 
-      Syntax.parse_term lthy1 rel_str
-      |> Type.constraint (rty --> rty --> @{typ bool}) 
-      |> Syntax.check_term lthy1 
-    val lthy2 = Variable.declare_term rel lthy1 
+    fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
+      let
+        val rty = Syntax.read_typ lthy rty_str
+        val lthy1 = Variable.declare_typ rty lthy
+        val rel =
+          Syntax.parse_term lthy1 rel_str
+          |> Type.constraint (rty --> rty --> @{typ bool})
+          |> Syntax.check_term lthy1
+        val lthy2 = Variable.declare_term rel lthy1
+      in
+        (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
+      end
+
+    val (spec', lthy') = fold_map parse_spec specs lthy
   in
-    (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
+    quotient_type spec' lthy'
   end
 
-  val (spec', lthy') = fold_map parse_spec specs lthy
-in
-  quotient_type spec' lthy'
-end
-
 val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
 
 val quotspec_parser =
@@ -299,8 +300,8 @@
 val _ = Keyword.keyword "/"
 
 val _ =
-    Outer_Syntax.local_theory_to_proof "quotient_type"
-      "quotient type definitions (require equivalence proofs)"
-         Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+  Outer_Syntax.local_theory_to_proof "quotient_type"
+    "quotient type definitions (require equivalence proofs)"
+       Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
 
 end; (* structure *)