tuned;
authorwenzelm
Mon, 19 Feb 2018 15:41:17 +0100
changeset 67667 e0c0a6bb265b
parent 67666 ad2b3e330c27
child 67668 23659b5dde1d
tuned;
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 =