# HG changeset patch
# User wenzelm
# Date 1519051277 -3600
# Node ID e0c0a6bb265bca86159d99cf63b882c284963d5d
# Parent  ad2b3e330c27568ecfc0b8626c63560e7be22250
tuned;

diff -r ad2b3e330c27 -r e0c0a6bb265b src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Feb 19 14:49:11 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Feb 19 15:41:17 2018 +0100
@@ -772,9 +772,7 @@
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
-fun is_hyp (elem as Assumes asms) = true
-  | is_hyp (elem as Defines defs) = true
-  | is_hyp _ = false;
+val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
 
 fun gen_add_locale prep_decl
     binding raw_predicate_binding raw_import raw_body thy =