--- 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