# HG changeset patch
# User wenzelm
# Date 1425894743 -3600
# Node ID 5d1b4ab7d173c930d6f3f5c9eae0ca8e764ba268
# Parent  e327a9ae2d610c62faeddca848772b532a6e5fb8
tuned;

diff -r e327a9ae2d61 -r 5d1b4ab7d173 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Sun Mar 08 22:09:25 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML	Mon Mar 09 10:52:23 2015 +0100
@@ -21,9 +21,6 @@
 structure Function_Elims : FUNCTION_ELIMS =
 struct
 
-open Function_Lib
-open Function_Common
-
 (* Extract a function and its arguments from a proposition that is
    either of the form "f x y z = ..." or, in case of function that
    returns a boolean, "f x y z" *)
@@ -78,7 +75,7 @@
 
 fun mk_partial_elim_rules ctxt result =
   let
-    val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
+    val Function_Common.FunctionResult {fs, R, dom, psimps, cases, ...} = result;
     val n_fs = length fs;
 
     fun variant_free used_term v =
@@ -138,9 +135,9 @@
           |> Thm.forall_intr (Thm.cterm_of ctxt rhs_var);
 
         val bool_elims =
-          (case fastype_of rhs_var of
-            Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
-          | _ => []);
+          if fastype_of rhs_var = @{typ bool}
+          then mk_bool_elims ctxt elim_stripped
+          else [];
 
         fun unstrip rl =
           rl