diff -r e5d82cf3c387 -r 4df6b0ae900d src/HOL/Tools/SMT/smt_util.ML
--- a/src/HOL/Tools/SMT/smt_util.ML	Tue Aug 29 16:24:14 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Tue Aug 29 18:30:23 2017 +0200
@@ -10,6 +10,8 @@
   val repeat: ('a -> 'a option) -> 'a -> 'a
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
+  datatype order = First_Order | Higher_Order
+
   (*class dictionaries*)
   type class = string list
   val basicC: class
@@ -79,6 +81,11 @@
   in rep end
 
 
+(* order *)
+
+datatype order = First_Order | Higher_Order
+
+
 (* class dictionaries *)
 
 type class = string list