# 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