--- a/src/HOL/Nitpick_Examples/minipick.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Nitpick_Examples/minipick.ML Sat Jan 05 17:24:33 2019 +0100
@@ -24,27 +24,27 @@
S_Rep |
R_Rep of bool
-fun check_type ctxt raw_infinite (Type (@{type_name fun}, Ts)) =
+fun check_type ctxt raw_infinite (Type (\<^type_name>\<open>fun\<close>, Ts)) =
List.app (check_type ctxt raw_infinite) Ts
- | check_type ctxt raw_infinite (Type (@{type_name prod}, Ts)) =
+ | check_type ctxt raw_infinite (Type (\<^type_name>\<open>prod\<close>, Ts)) =
List.app (check_type ctxt raw_infinite) Ts
- | check_type _ _ @{typ bool} = ()
- | check_type _ _ (TFree (_, @{sort "{}"})) = ()
- | check_type _ _ (TFree (_, @{sort HOL.type})) = ()
+ | check_type _ _ \<^typ>\<open>bool\<close> = ()
+ | check_type _ _ (TFree (_, \<^sort>\<open>{}\<close>)) = ()
+ | check_type _ _ (TFree (_, \<^sort>\<open>HOL.type\<close>)) = ()
| check_type ctxt raw_infinite T =
if raw_infinite T then
()
else
error ("Not supported: Type " ^ quote (Syntax.string_of_typ ctxt T) ^ ".")
-fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
+fun atom_schema_of S_Rep card (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
replicate_list (card T1) (atom_schema_of S_Rep card T2)
| atom_schema_of (R_Rep true) card
- (Type (@{type_name fun}, [T1, @{typ bool}])) =
+ (Type (\<^type_name>\<open>fun\<close>, [T1, \<^typ>\<open>bool\<close>])) =
atom_schema_of S_Rep card T1
- | atom_schema_of (rep as R_Rep _) card (Type (@{type_name fun}, [T1, T2])) =
+ | atom_schema_of (rep as R_Rep _) card (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
atom_schema_of S_Rep card T1 @ atom_schema_of rep card T2
- | atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
+ | atom_schema_of _ card (Type (\<^type_name>\<open>prod\<close>, Ts)) =
maps (atom_schema_of S_Rep card) Ts
| atom_schema_of _ card T = [card T]
val arity_of = length ooo atom_schema_of
@@ -79,7 +79,7 @@
fun S_rep_from_F NONE f = RelIf (f, true_atom, false_atom)
| S_rep_from_F (SOME true) f = RelIf (f, true_atom, None)
| S_rep_from_F (SOME false) f = RelIf (Not f, false_atom, None)
- fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
+ fun R_rep_from_S_rep (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) r =
if total andalso T2 = bool_T then
let
val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
@@ -109,12 +109,12 @@
|> foldl1 Union
end
| R_rep_from_S_rep _ r = r
- fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
+ fun S_rep_from_R_rep Ts (T as Type (\<^type_name>\<open>fun\<close>, _)) r =
Comprehension (decls_for S_Rep card Ts T,
RelEq (R_rep_from_S_rep T
(rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
| S_rep_from_R_rep _ _ r = r
- fun partial_eq pos Ts (Type (@{type_name fun}, [T1, T2])) t1 t2 =
+ fun partial_eq pos Ts (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) t1 t2 =
HOLogic.mk_all ("x", T1,
HOLogic.eq_const T2 $ (incr_boundvars 1 t1 $ Bound 0)
$ (incr_boundvars 1 t2 $ Bound 0))
@@ -127,26 +127,26 @@
|> (if pos then Some o Intersect else Lone o Union)
and to_F pos Ts t =
(case t of
- @{const Not} $ t1 => Not (to_F (Option.map not pos) Ts t1)
- | @{const False} => False
- | @{const True} => True
- | Const (@{const_name All}, _) $ Abs (_, T, t') =>
+ \<^const>\<open>Not\<close> $ t1 => Not (to_F (Option.map not pos) Ts t1)
+ | \<^const>\<open>False\<close> => False
+ | \<^const>\<open>True\<close> => True
+ | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, T, t') =>
if pos = SOME true andalso not (complete T) then False
else All (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
- | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
to_F pos Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
+ | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, T, t') =>
if pos = SOME false andalso not (complete T) then True
else Exist (decls_for S_Rep card Ts T, to_F pos (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
to_F pos Ts (t0 $ eta_expand Ts t1 1)
- | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
+ | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) $ t1 $ t2 =>
(case pos of
NONE => RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
| SOME pos => partial_eq pos Ts T t1 t2)
- | Const (@{const_name ord_class.less_eq},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [T', @{typ bool}]), _]))
+ | Const (\<^const_name>\<open>ord_class.less_eq\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [T', \<^typ>\<open>bool\<close>]), _]))
$ t1 $ t2 =>
(case pos of
NONE => Subset (to_R_rep Ts t1, to_R_rep Ts t2)
@@ -158,11 +158,11 @@
Subset (Join (to_R_rep Ts t1, true_atom),
Difference (atom_seq_product_of S_Rep card T',
Join (to_R_rep Ts t2, false_atom))))
- | @{const HOL.conj} $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
- | @{const HOL.disj} $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
- | @{const HOL.implies} $ t1 $ t2 =>
+ | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => And (to_F pos Ts t1, to_F pos Ts t2)
+ | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => Or (to_F pos Ts t1, to_F pos Ts t2)
+ | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
Implies (to_F (Option.map not pos) Ts t1, to_F pos Ts t2)
- | Const (@{const_name Set.member}, _) $ t1 $ t2 => to_F pos Ts (t2 $ t1)
+ | Const (\<^const_name>\<open>Set.member\<close>, _) $ t1 $ t2 => to_F pos Ts (t2 $ t1)
| t1 $ t2 =>
(case pos of
NONE => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
@@ -181,22 +181,22 @@
handle SAME () => F_from_S_rep pos (to_R_rep Ts t)
and to_S_rep Ts t =
case t of
- Const (@{const_name Pair}, _) $ t1 $ t2 =>
+ Const (\<^const_name>\<open>Pair\<close>, _) $ t1 $ t2 =>
Product (to_S_rep Ts t1, to_S_rep Ts t2)
- | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name fst}, _) $ t1 =>
+ | Const (\<^const_name>\<open>Pair\<close>, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>Pair\<close>, _) => to_S_rep Ts (eta_expand Ts t 2)
+ | Const (\<^const_name>\<open>fst\<close>, _) $ t1 =>
let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in
Project (to_S_rep Ts t1, num_seq 0 fst_arity)
end
- | Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name snd}, _) $ t1 =>
+ | Const (\<^const_name>\<open>fst\<close>, _) => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>snd\<close>, _) $ t1 =>
let
val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))
val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))
val fst_arity = pair_arity - snd_arity
in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
- | Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>snd\<close>, _) => to_S_rep Ts (eta_expand Ts t 1)
| Bound j => rel_expr_for_bound_var card S_Rep Ts j
| _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
and partial_set_op swap1 swap2 op1 op2 Ts t1 t2 =
@@ -211,37 +211,37 @@
end
and to_R_rep Ts t =
(case t of
- @{const Not} => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name ord_class.less_eq},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
+ \<^const>\<open>Not\<close> => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>All\<close>, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>Ex\<close>, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>HOL.eq\<close>, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (\<^const_name>\<open>ord_class.less_eq\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [_, \<^typ>\<open>bool\<close>]), _])) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name ord_class.less_eq}, _) =>
+ | Const (\<^const_name>\<open>ord_class.less_eq\<close>, _) =>
to_R_rep Ts (eta_expand Ts t 2)
- | @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
- | @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name Set.member}, _) $ _ =>
+ | \<^const>\<open>HOL.conj\<close> $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | \<^const>\<open>HOL.conj\<close> => to_R_rep Ts (eta_expand Ts t 2)
+ | \<^const>\<open>HOL.disj\<close> $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | \<^const>\<open>HOL.disj\<close> => to_R_rep Ts (eta_expand Ts t 2)
+ | \<^const>\<open>HOL.implies\<close> $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | \<^const>\<open>HOL.implies\<close> => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (\<^const_name>\<open>Set.member\<close>, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name Set.member}, _) => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name Collect}, _) $ t' => to_R_rep Ts t'
- | Const (@{const_name Collect}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name bot_class.bot},
- T as Type (@{type_name fun}, [T', @{typ bool}])) =>
+ | Const (\<^const_name>\<open>Set.member\<close>, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (\<^const_name>\<open>Collect\<close>, _) $ t' => to_R_rep Ts t'
+ | Const (\<^const_name>\<open>Collect\<close>, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>bot_class.bot\<close>,
+ T as Type (\<^type_name>\<open>fun\<close>, [T', \<^typ>\<open>bool\<close>])) =>
if total then empty_n_ary_rel (arity_of (R_Rep total) card T)
else Product (atom_seq_product_of (R_Rep total) card T', false_atom)
- | Const (@{const_name top_class.top},
- T as Type (@{type_name fun}, [T', @{typ bool}])) =>
+ | Const (\<^const_name>\<open>top_class.top\<close>,
+ T as Type (\<^type_name>\<open>fun\<close>, [T', \<^typ>\<open>bool\<close>])) =>
if total then atom_seq_product_of (R_Rep total) card T
else Product (atom_seq_product_of (R_Rep total) card T', true_atom)
- | Const (@{const_name insert}, Type (_, [T, _])) $ t1 $ t2 =>
+ | Const (\<^const_name>\<open>insert\<close>, Type (_, [T, _])) $ t1 $ t2 =>
if total then
Union (to_S_rep Ts t1, to_R_rep Ts t2)
else
@@ -258,9 +258,9 @@
Difference (kt2, Product (atom_seq_product_of S_Rep card T,
false_atom)))
end
- | Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name trancl},
+ | Const (\<^const_name>\<open>insert\<close>, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>insert\<close>, _) => to_R_rep Ts (eta_expand Ts t 2)
+ | Const (\<^const_name>\<open>trancl\<close>,
Type (_, [Type (_, [Type (_, [T', _]), _]), _])) $ t1 =>
if arity_of S_Rep card T' = 1 then
if total then
@@ -281,57 +281,57 @@
end
else
error "Not supported: Transitive closure for function or pair type."
- | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name inf_class.inf},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ | Const (\<^const_name>\<open>trancl\<close>, _) => to_R_rep Ts (eta_expand Ts t 1)
+ | Const (\<^const_name>\<open>inf_class.inf\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [_, \<^typ>\<open>bool\<close>]), _]))
$ t1 $ t2 =>
if total then Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
else partial_set_op true true Intersect Union Ts t1 t2
- | Const (@{const_name inf_class.inf}, _) $ _ =>
+ | Const (\<^const_name>\<open>inf_class.inf\<close>, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name inf_class.inf}, _) =>
+ | Const (\<^const_name>\<open>inf_class.inf\<close>, _) =>
to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name sup_class.sup},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ | Const (\<^const_name>\<open>sup_class.sup\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [_, \<^typ>\<open>bool\<close>]), _]))
$ t1 $ t2 =>
if total then Union (to_R_rep Ts t1, to_R_rep Ts t2)
else partial_set_op true true Union Intersect Ts t1 t2
- | Const (@{const_name sup_class.sup}, _) $ _ =>
+ | Const (\<^const_name>\<open>sup_class.sup\<close>, _) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name sup_class.sup}, _) =>
+ | Const (\<^const_name>\<open>sup_class.sup\<close>, _) =>
to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+ | Const (\<^const_name>\<open>minus_class.minus\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [_, \<^typ>\<open>bool\<close>]), _]))
$ t1 $ t2 =>
if total then Difference (to_R_rep Ts t1, to_R_rep Ts t2)
else partial_set_op true false Intersect Union Ts t1 t2
- | Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
+ | Const (\<^const_name>\<open>minus_class.minus\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [_, \<^typ>\<open>bool\<close>]), _])) $ _ =>
to_R_rep Ts (eta_expand Ts t 1)
- | Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
+ | Const (\<^const_name>\<open>minus_class.minus\<close>,
+ Type (\<^type_name>\<open>fun\<close>,
+ [Type (\<^type_name>\<open>fun\<close>, [_, \<^typ>\<open>bool\<close>]), _])) =>
to_R_rep Ts (eta_expand Ts t 2)
- | Const (@{const_name Pair}, _) $ _ $ _ => to_S_rep Ts t
- | Const (@{const_name Pair}, _) $ _ => to_S_rep Ts t
- | Const (@{const_name Pair}, _) => to_S_rep Ts t
- | Const (@{const_name fst}, _) $ _ => raise SAME ()
- | Const (@{const_name fst}, _) => raise SAME ()
- | Const (@{const_name snd}, _) $ _ => raise SAME ()
- | Const (@{const_name snd}, _) => raise SAME ()
- | @{const False} => false_atom
- | @{const True} => true_atom
+ | Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ _ => to_S_rep Ts t
+ | Const (\<^const_name>\<open>Pair\<close>, _) $ _ => to_S_rep Ts t
+ | Const (\<^const_name>\<open>Pair\<close>, _) => to_S_rep Ts t
+ | Const (\<^const_name>\<open>fst\<close>, _) $ _ => raise SAME ()
+ | Const (\<^const_name>\<open>fst\<close>, _) => raise SAME ()
+ | Const (\<^const_name>\<open>snd\<close>, _) $ _ => raise SAME ()
+ | Const (\<^const_name>\<open>snd\<close>, _) => raise SAME ()
+ | \<^const>\<open>False\<close> => false_atom
+ | \<^const>\<open>True\<close> => true_atom
| Free (x as (_, T)) =>
Rel (arity_of (R_Rep total) card T, find_index (curry (op =) x) frees)
| Term.Var _ => error "Not supported: Schematic variables."
| Bound _ => raise SAME ()
| Abs (_, T, t') =>
(case (total, fastype_of1 (T :: Ts, t')) of
- (true, @{typ bool}) =>
+ (true, \<^typ>\<open>bool\<close>) =>
Comprehension (decls_for S_Rep card Ts T, to_F NONE (T :: Ts) t')
| (_, T') =>
Comprehension (decls_for S_Rep card Ts T @
@@ -341,7 +341,7 @@
to_R_rep (T :: Ts) t')))
| t1 $ t2 =>
(case fastype_of1 (Ts, t) of
- @{typ bool} =>
+ \<^typ>\<open>bool\<close> =>
if total then
S_rep_from_F NONE (to_F NONE Ts t)
else
@@ -374,7 +374,7 @@
end
fun declarative_axiom_for_rel_expr total card Ts
- (Type (@{type_name fun}, [T1, T2])) r =
+ (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) r =
if total andalso body_type T2 = bool_T then
True
else
@@ -388,28 +388,28 @@
(Rel (arity_of (R_Rep total) card T, i))
(* Hack to make the old code work as is with sets. *)
-fun unsetify_type (Type (@{type_name set}, [T])) = unsetify_type T --> bool_T
+fun unsetify_type (Type (\<^type_name>\<open>set\<close>, [T])) = unsetify_type T --> bool_T
| unsetify_type (Type (s, Ts)) = Type (s, map unsetify_type Ts)
| unsetify_type T = T
fun kodkod_problem_from_term ctxt total raw_card raw_infinite t =
let
val thy = Proof_Context.theory_of ctxt
- fun card (Type (@{type_name fun}, [T1, T2])) =
+ fun card (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
reasonable_power (card T2) (card T1)
- | card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
- | card @{typ bool} = 2
+ | card (Type (\<^type_name>\<open>prod\<close>, [T1, T2])) = card T1 * card T2
+ | card \<^typ>\<open>bool\<close> = 2
| card T = Int.max (1, raw_card T)
- fun complete (Type (@{type_name fun}, [T1, T2])) =
+ fun complete (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
concrete T1 andalso complete T2
- | complete (Type (@{type_name prod}, Ts)) = forall complete Ts
+ | complete (Type (\<^type_name>\<open>prod\<close>, Ts)) = forall complete Ts
| complete T = not (raw_infinite T)
- and concrete (Type (@{type_name fun}, [T1, T2])) =
+ and concrete (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
complete T1 andalso concrete T2
- | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
+ | concrete (Type (\<^type_name>\<open>prod\<close>, Ts)) = forall concrete Ts
| concrete _ = true
val neg_t =
- @{const Not} $ Object_Logic.atomize_term ctxt t
+ \<^const>\<open>Not\<close> $ Object_Logic.atomize_term ctxt t
|> map_types unsetify_type
val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
val frees = Term.add_frees neg_t []
@@ -445,7 +445,7 @@
| Error (s, _) => error ("Kodkod error: " ^ s)
end
-val default_raw_infinite = member (op =) [@{typ nat}, @{typ int}]
+val default_raw_infinite = member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>]
fun minipick ctxt n t =
let