# HG changeset patch
# User krauss
# Date 1378681185 -7200
# Node ID dde3cc2804cc5b6ef2f9c0039e80d5a6b751e88b
# Parent  0f472e7063afbffe2a338a8c075ad7cbd388309a
dropped unnecessary 'open'

diff -r 0f472e7063af -r dde3cc2804cc src/HOL/Tools/Function/fun_cases.ML
--- 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;