# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1268578217 -3600
# Node ID a9507cd843260683bd9dbc9f4588efaf23117a7c
# Parent  a2b163256f9b0aa569f0a4fd7dbbf0c52c0ed9f6
removed Local_Theory.theory_result by using local Typedef.add_typedef

diff -r a2b163256f9b -r a9507cd84326 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Mar 14 14:36:56 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Mar 14 15:50:17 2010 +0100
@@ -1,7 +1,8 @@
-(*  Title:      HOL/Tools/Quotient/quotient_typ.thy
+(*  Title:      quotient_typ.thy
     Author:     Cezary Kaliszyk and Christian Urban
 
-Definition of a quotient type.
+    Definition of a quotient type.
+
 *)
 
 signature QUOTIENT_TYPE =
@@ -71,13 +72,10 @@
 fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
 let
   val typedef_tac =
-     EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
+    EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
-  Local_Theory.theory_result
-    (Typedef.add_typedef_global false NONE
-       (qty_name, vs, mx)
-          (typedef_term rel rty lthy)
-             NONE typedef_tac) lthy
+  Typedef.add_typedef false NONE (qty_name, vs, mx) 
+    (typedef_term rel rty lthy) NONE typedef_tac lthy
 end
 
 
@@ -275,17 +273,13 @@
 let
   fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
   let
-    (* new parsing with proper declaration *)
     val rty = Syntax.read_typ lthy rty_str
     val lthy1 = Variable.declare_typ rty lthy
-    val pre_rel = Syntax.parse_term lthy1 rel_str
-    val pre_rel' = Syntax.type_constraint (rty --> rty --> @{typ bool}) pre_rel
-    val rel = Syntax.check_term lthy1 pre_rel'
-    val lthy2 = Variable.declare_term rel lthy1
-
-    (* old parsing *)
-    (* val rty = Syntax.read_typ lthy rty_str
-       val rel = Syntax.read_term lthy rel_str *)
+    val rel = 
+      Syntax.parse_term lthy1 rel_str
+      |> Syntax.type_constraint (rty --> rty --> @{typ bool}) 
+      |> Syntax.check_term lthy1 
+    val lthy2 = Variable.declare_term rel lthy1 
   in
     (((vs, qty_name, mx), (rty, rel)), lthy2)
   end