# HG changeset patch
# User wenzelm
# Date 1319746855 -7200
# Node ID eaec1651709ab332a5e99cc38a863829ac9bc381
# Parent  29e88714ffe4e740d4b2af969f5467d411b23656
eliminated aliases of standard functions;

diff -r 29e88714ffe4 -r eaec1651709a src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 21:52:57 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Thu Oct 27 22:20:55 2011 +0200
@@ -19,31 +19,6 @@
 structure Quotient_Type: QUOTIENT_TYPE =
 struct
 
-(* wrappers for define, note, Attrib.internal and theorem_i *)  (* FIXME !? *)
-
-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
-
-fun note (name, thm, attrs) lthy =
-  Local_Theory.note ((name, attrs), [thm]) lthy |> snd
-
-
-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
-
-
 
 (*** definition of quotient types ***)
 
@@ -145,8 +120,10 @@
     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) = lthy1
+      |> Local_Theory.define ((abs_name, NoSyn), (Attrib.empty_binding, abs_trm))
+    val ((_, (_, rep_def)), lthy3) = lthy2
+      |> Local_Theory.define ((rep_name, NoSyn), (Attrib.empty_binding, rep_trm))
 
     (* quot_type theorem *)
     val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
@@ -168,10 +145,13 @@
     val lthy4 = lthy3
       |> Local_Theory.declaration true
         (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
-      |> note
-        (equiv_thm_name, equiv_thm,
-          if partial then [] else [intern_attr Quotient_Info.equiv_rules_add])
-      |> note (quotient_thm_name, quotient_thm, [intern_attr Quotient_Info.quotient_rules_add])
+      |> (snd oo Local_Theory.note)
+        ((equiv_thm_name,
+          if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
+          [equiv_thm])
+      |> (snd oo Local_Theory.note)
+        ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
+          [quotient_thm])
   in
     (quotients, lthy4)
   end
@@ -267,10 +247,9 @@
 
     val goals = map (mk_goal o snd) quot_list
 
-    fun after_qed thms lthy =
-      fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
+    fun after_qed [thms] = fold (snd oo add_quotient_type) (quot_list ~~ thms)
   in
-    theorem after_qed goals lthy
+    Proof.theorem NONE after_qed [map (rpair []) goals] lthy
   end
 
 fun quotient_type_cmd specs lthy =