# HG changeset patch
# User haftmann
# Date 1285322184 -7200
# Node ID b4cbc72a354cc8fef2b2b3bc109e49123d0a7c07
# Parent  fabd6b48fe6e887e94b2068f908c90a492724061# Parent  dacf4bad3954ad46ced98e3754892a15720c11ed
merged

diff -r dacf4bad3954 -r b4cbc72a354c src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Sep 24 11:56:14 2010 +0200
+++ b/src/HOL/Quotient.thy	Fri Sep 24 11:56:24 2010 +0200
@@ -661,6 +661,17 @@
   shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
   by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
 
+lemma id_rsp:
+  shows "(R ===> R) id id"
+  by simp
+
+lemma id_prs:
+  assumes a: "Quotient R Abs Rep"
+  shows "(Rep ---> Abs) id = id"
+  unfolding fun_eq_iff
+  by (simp add: Quotient_abs_rep[OF a])
+
+
 locale quot_type =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -731,8 +742,8 @@
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp
-lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
+lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
 lemmas [quot_equiv] = identity_equivp
 
 
diff -r dacf4bad3954 -r b4cbc72a354c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 11:56:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 11:56:24 2010 +0200
@@ -431,7 +431,8 @@
 fun check_matches_type ctxt predname T ms =
   let
     fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
-      | check m (Type("fun", _)) = false
+      | check m (T as Type("fun", _)) =
+        if body_type T = @{typ bool} then false else (m = Input orelse m = Output)
       | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
           check m1 T1 andalso check m2 T2 
       | check Input T = true
diff -r dacf4bad3954 -r b4cbc72a354c src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Fri Sep 24 11:56:14 2010 +0200
+++ b/src/Tools/Metis/metis.ML	Fri Sep 24 11:56:24 2010 +0200
@@ -12752,7 +12752,7 @@
 
 fun ppEquation (_,th) = Metis_Thm.pp th;
 
-val equationToString = Metis_Print.toString ppEquation;
+fun equationToString x = Metis_Print.toString ppEquation x;
 
 fun equationLiteral (t_u,th) =
     let
@@ -18364,7 +18364,7 @@
         rw
       end;
 
-val addList = List.foldl (fn (eqn,rw) => add rw eqn);
+fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
 
 (* ------------------------------------------------------------------------- *)
 (* Rewriting (the order must be a refinement of the rewrite order).          *)
@@ -18824,7 +18824,7 @@
     end;
 end;
 
-val rewrite = orderedRewrite (K (SOME GREATER));
+fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
 
 end
 
diff -r dacf4bad3954 -r b4cbc72a354c src/Tools/Metis/src/Rewrite.sml
--- a/src/Tools/Metis/src/Rewrite.sml	Fri Sep 24 11:56:14 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml	Fri Sep 24 11:56:24 2010 +0200
@@ -207,7 +207,7 @@
         rw
       end;
 
-val addList = List.foldl (fn (eqn,rw) => add rw eqn);
+fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
 
 (* ------------------------------------------------------------------------- *)
 (* Rewriting (the order must be a refinement of the rewrite order).          *)
@@ -667,6 +667,6 @@
     end;
 end;
 
-val rewrite = orderedRewrite (K (SOME GREATER));
+fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
 
 end
diff -r dacf4bad3954 -r b4cbc72a354c src/Tools/Metis/src/Rule.sml
--- a/src/Tools/Metis/src/Rule.sml	Fri Sep 24 11:56:14 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sml	Fri Sep 24 11:56:24 2010 +0200
@@ -96,7 +96,7 @@
 
 fun ppEquation (_,th) = Thm.pp th;
 
-val equationToString = Print.toString ppEquation;
+fun equationToString x = Print.toString ppEquation x;
 
 fun equationLiteral (t_u,th) =
     let