# HG changeset patch
# User bulwahn
# Date 1320082165 -3600
# Node ID bf8b9ac6000ccf874f7f3f01f3c082a0a2bdb003
# Parent  97b77157900072051cbb793acffcfbd200b4f949
more robust, declarative and unsurprising computation of types in the quotient type definition

diff -r 97b771579000 -r bf8b9ac6000c src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Oct 31 08:50:35 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Oct 31 18:29:25 2011 +0100
@@ -79,10 +79,9 @@
 (* 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
+    val quot_type_const = Const (@{const_name "quot_type"},
+      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
+    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
   in
     Goal.prove lthy [] [] goal
       (K (typedef_quot_type_tac equiv_thm typedef_info))
@@ -109,10 +108,11 @@
     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_const = Const (@{const_name quot_type.abs},
+      (rty --> rty --> @{typ bool}) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
+    val rep_const = Const (@{const_name quot_type.rep}, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
+    val abs_trm = abs_const $ rel $ Abs_const
+    val rep_trm = rep_const $ Rep_const
     val abs_name = Binding.prefix_name "abs_" qty_name
     val rep_name = Binding.prefix_name "rep_" qty_name