# HG changeset patch
# User haftmann
# Date 1267018948 -3600
# Node ID f759782e35ac1a5fea6f1eae6003e7e055e8ef98
# Parent  ca158c7b1144af96557ee0f7f40d929f56e98cbf
bound argument for abstype proposition

diff -r ca158c7b1144 -r f759782e35ac src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Feb 24 14:34:40 2010 +0100
+++ b/src/HOL/Rat.thy	Wed Feb 24 14:42:28 2010 +0100
@@ -1020,7 +1020,8 @@
 
 code_abstype Frct quotient_of
 proof (rule eq_reflection)
-  show "Frct (quotient_of x) = x" by (cases x) (auto intro: quotient_of_eq)
+  fix r :: rat
+  show "Frct (quotient_of r) = r" by (cases r) (auto intro: quotient_of_eq)
 qed
 
 lemma Frct_code_post [code_post]:
diff -r ca158c7b1144 -r f759782e35ac src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Feb 24 14:34:40 2010 +0100
+++ b/src/Pure/Isar/code.ML	Wed Feb 24 14:42:28 2010 +0100
@@ -422,8 +422,9 @@
           ^ " :: " ^ string_of_typ thy ty');
     val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle TYPE _ =>
       error ("Not a projection:\n" ^ string_of_const thy rep);
-    val cert = Logic.mk_equals (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty)
-      $ Free ("x", ty_abs)), Free ("x", ty_abs));
+    val param = Free ("x", ty_abs);
+    val cert = Logic.all param (Logic.mk_equals
+      (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty) $ param), param));
   in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;    
 
 fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)