--- a/src/HOL/Tools/Function/fun_cases.ML Mon Sep 09 00:53:50 2013 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML Mon Sep 09 00:59:45 2013 +0200
@@ -15,7 +15,6 @@
struct
local
- open Function_Elims;
val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
(fn _ => assume_tac 1);
@@ -31,7 +30,7 @@
error (Pretty.string_of (Pretty.block
[Pretty.str "Proposition is not a function equation:",
Pretty.fbrk, Syntax.pretty_term ctxt prop]));
- val ((f,_),_) = dest_funprop (HOLogic.dest_Trueprop prop)
+ val ((f,_),_) = Function_Elims.dest_funprop (HOLogic.dest_Trueprop prop)
handle TERM _ => err ();
val info = Function.get_info ctxt f handle Empty => err ();
val {elims, pelims, is_partial, ...} = info;