--- a/src/ZF/Datatype.thy Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Datatype.thy Sat Sep 11 22:02:12 2021 +0200
@@ -63,7 +63,7 @@
struct
val trace = Unsynchronized.ref false;
- fun mk_new ([],[]) = Const(\<^const_name>\<open>True\<close>,FOLogic.oT)
+ fun mk_new ([],[]) = \<^Const>\<open>True\<close>
| mk_new (largs,rargs) =
Balanced_Tree.make FOLogic.mk_conj
(map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
@@ -89,7 +89,7 @@
if #big_rec_name lcon_info = #big_rec_name rcon_info
andalso not (null (#free_iffs lcon_info)) then
if lname = rname then mk_new (largs, rargs)
- else Const(\<^const_name>\<open>False\<close>,FOLogic.oT)
+ else \<^Const>\<open>False\<close>
else raise Match
val _ =
if !trace then writeln ("NEW = " ^ Syntax.string_of_term ctxt new)
--- a/src/ZF/Tools/datatype_package.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML Sat Sep 11 22:02:12 2021 +0200
@@ -187,7 +187,7 @@
(*Find each recursive argument and add a recursive call for it*)
fun rec_args [] = []
- | rec_args ((Const(\<^const_name>\<open>mem\<close>,_)$arg$X)::prems) =
+ | rec_args (\<^Const_>\<open>mem for arg X\<close>::prems) =
(case head_of X of
Const(a,_) => (*recursive occurrence?*)
if member (op =) rec_names a
@@ -310,7 +310,7 @@
| SOME recursor_def =>
let
(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
- fun subst_rec (Const(\<^const_name>\<open>apply\<close>,_) $ Free _ $ arg) = recursor_tm $ arg
+ fun subst_rec \<^Const_>\<open>apply for \<open>Free _\<close> arg\<close> = recursor_tm $ arg
| subst_rec tm =
let val (head, args) = strip_comb tm
in list_comb (head, map subst_rec args) end;
--- a/src/ZF/Tools/induct_tacs.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Sat Sep 11 22:02:12 2021 +0200
@@ -70,8 +70,7 @@
exception Find_tname of string
fun find_tname ctxt var As =
- let fun mk_pair (Const(\<^const_name>\<open>mem\<close>,_) $ Free (v,_) $ A) =
- (v, #1 (dest_Const (head_of A)))
+ let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
| mk_pair _ = raise Match
val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
val x =
@@ -99,7 +98,7 @@
datatype_info thy tn
|> (if exh then #exhaustion else #induct)
|> Thm.transfer thy;
- val (Const(\<^const_name>\<open>mem\<close>,_) $ Var(ixn,_) $ _) =
+ val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
(case Thm.prems_of rule of
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
@@ -120,15 +119,14 @@
fun rep_datatype_i elim induct case_eqns recursor_eqns thy =
let
(*analyze the LHS of a case equation to get a constructor*)
- fun const_of (Const(\<^const_name>\<open>IFOL.eq\<close>, _) $ (_ $ c) $ _) = c
+ fun const_of \<^Const_>\<open>IFOL.eq _ for \<open>_ $ c\<close> _\<close> = c
| const_of eqn = error ("Ill-formed case equation: " ^
Syntax.string_of_term_global thy eqn);
val constructors =
map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
- val Const (\<^const_name>\<open>mem\<close>, _) $ _ $ data =
- FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
+ val \<^Const_>\<open>mem for _ data\<close> = FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
val Const(big_rec_name, _) = head_of data;
--- a/src/ZF/Tools/inductive_package.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Sep 11 22:02:12 2021 +0200
@@ -99,7 +99,7 @@
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
- fun dest_tprop (Const(\<^const_name>\<open>Trueprop\<close>,_) $ P) = P
+ fun dest_tprop \<^Const_>\<open>Trueprop for P\<close> = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
Syntax.string_of_term ctxt0 Q);
@@ -297,8 +297,7 @@
(*Used to make induction rules;
ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
prem is a premise of an intr rule*)
- fun add_induct_prem ind_alist (prem as Const (\<^const_name>\<open>Trueprop\<close>, _) $
- (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X), iprems) =
+ fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
(case AList.lookup (op aconv) ind_alist X of
SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
@@ -514,7 +513,7 @@
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
- val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (pred_var $ _) = Thm.concl_of induct0
+ val \<^Const_>\<open>Trueprop for \<open>pred_var $ _\<close>\<close> = Thm.concl_of induct0
val induct0 =
CP.split_rule_var ctxt4
--- a/src/ZF/Tools/primrec_package.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sat Sep 11 22:02:12 2021 +0200
@@ -115,8 +115,7 @@
case AList.lookup (op =) eqns cname of
NONE => (warning ("no equation for constructor " ^ cname ^
"\nin definition of function " ^ fname);
- (Const (\<^const_name>\<open>zero\<close>, Ind_Syntax.iT),
- #2 recursor_pair, Const (\<^const_name>\<open>zero\<close>, Ind_Syntax.iT)))
+ (\<^Const>\<open>zero\<close>, #2 recursor_pair, \<^Const>\<open>zero\<close>))
| SOME (rhs, cargs', eq) =>
(rhs, inst_recursor (recursor_pair, cargs'), eq)
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs))
--- a/src/ZF/Tools/typechk.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/Tools/typechk.ML Sat Sep 11 22:02:12 2021 +0200
@@ -76,8 +76,7 @@
if length rls <= maxr then resolve_tac ctxt rls i else no_tac
end);
-fun is_rigid_elem (Const(\<^const_name>\<open>Trueprop\<close>,_) $ (Const(\<^const_name>\<open>mem\<close>,_) $ a $ _)) =
- not (is_Var (head_of a))
+fun is_rigid_elem \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for a _\<close>\<close>\<close> = not (is_Var (head_of a))
| is_rigid_elem _ = false;
(*Try solving a:A by assumption provided a is rigid!*)
--- a/src/ZF/arith_data.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/arith_data.ML Sat Sep 11 22:02:12 2021 +0200
@@ -24,8 +24,8 @@
val iT = Ind_Syntax.iT;
-val zero = Const(\<^const_name>\<open>zero\<close>, iT);
-val succ = Const(\<^const_name>\<open>succ\<close>, iT --> iT);
+val zero = \<^Const>\<open>zero\<close>;
+val succ = \<^Const>\<open>succ\<close>;
fun mk_succ t = succ $ t;
val one = mk_succ zero;
@@ -44,9 +44,9 @@
(* dest_sum *)
-fun dest_sum (Const(\<^const_name>\<open>zero\<close>,_)) = []
- | dest_sum (Const(\<^const_name>\<open>succ\<close>,_) $ t) = one :: dest_sum t
- | dest_sum (Const(\<^const_name>\<open>Arith.add\<close>,_) $ t $ u) = dest_sum t @ dest_sum u
+fun dest_sum \<^Const_>\<open>zero\<close> = []
+ | dest_sum \<^Const_>\<open>succ for t\<close> = one :: dest_sum t
+ | dest_sum \<^Const_>\<open>Arith.add for t u\<close> = dest_sum t @ dest_sum u
| dest_sum tm = [tm];
(*Apply the given rewrite (if present) just once*)
--- a/src/ZF/ind_syntax.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/ind_syntax.ML Sat Sep 11 22:02:12 2021 +0200
@@ -18,7 +18,7 @@
(** Abstract syntax definitions for ZF **)
-val iT = Type(\<^type_name>\<open>i\<close>, []);
+val iT = \<^Type>\<open>i\<close>;
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
fun mk_all_imp (A,P) =
@@ -29,17 +29,16 @@
fun mk_Collect (a, D, t) = \<^const>\<open>Collect\<close> $ D $ absfree (a, iT) t;
(*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _) =
+fun chk_prem rec_hd \<^Const_>\<open>conj for _ _\<close> =
error"Premises may not be conjuctive"
- | chk_prem rec_hd (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X) =
+ | chk_prem rec_hd \<^Const_>\<open>mem for t X\<close> =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
| chk_prem rec_hd t =
(Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
(*Return the conclusion of a rule, of the form t:X*)
fun rule_concl rl =
- let val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>mem\<close>, _) $ t $ X) =
- Logic.strip_imp_concl rl
+ let val \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close> = Logic.strip_imp_concl rl
in (t,X) end;
(*As above, but return error message if bad*)
@@ -61,7 +60,7 @@
type constructor_spec =
(string * typ * mixfix) * string * term list * term list;
-fun dest_mem (Const (\<^const_name>\<open>mem\<close>, _) $ x $ A) = (x, A)
+fun dest_mem \<^Const_>\<open>mem for x A\<close> = (x, A)
| dest_mem _ = error "Constructor specifications must have the form x:A";
(*read a constructor specification*)
--- a/src/ZF/int_arith.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/int_arith.ML Sat Sep 11 22:02:12 2021 +0200
@@ -44,7 +44,7 @@
fun mk_numeral i = \<^const>\<open>integ_of\<close> $ mk_bin i;
-fun dest_numeral (Const(\<^const_name>\<open>integ_of\<close>, _) $ w) = dest_bin w
+fun dest_numeral \<^Const_>\<open>integ_of for w\<close> = dest_bin w
| dest_numeral t = raise TERM ("dest_numeral", [t]);
fun find_first_numeral past (t::terms) =
@@ -65,9 +65,9 @@
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
(*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const (\<^const_name>\<open>zadd\<close>, _) $ t $ u, ts) =
+fun dest_summing (pos, \<^Const_>\<open>zadd for t u\<close>, ts) =
dest_summing (pos, t, dest_summing (pos, u, ts))
- | dest_summing (pos, Const (\<^const_name>\<open>zdiff\<close>, _) $ t $ u, ts) =
+ | dest_summing (pos, \<^Const_>\<open>zdiff for t u\<close>, ts) =
dest_summing (pos, t, dest_summing (not pos, u, ts))
| dest_summing (pos, t, ts) =
if pos then t::ts else \<^const>\<open>zminus\<close> $ t :: ts;
@@ -93,7 +93,7 @@
fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
(*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const (\<^const_name>\<open>zminus\<close>, _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign \<^Const_>\<open>zminus for t\<close> = dest_coeff (~sign) t
| dest_coeff sign t =
let val ts = sort Term_Ord.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
--- a/src/ZF/simpdata.ML Sat Sep 11 21:58:02 2021 +0200
+++ b/src/ZF/simpdata.ML Sat Sep 11 22:02:12 2021 +0200
@@ -19,11 +19,11 @@
| NONE => [th])
| _ => [th]
in case Thm.concl_of th of
- Const(\<^const_name>\<open>Trueprop\<close>,_) $ P =>
+ \<^Const_>\<open>Trueprop for P\<close> =>
(case P of
- Const(\<^const_name>\<open>mem\<close>,_) $ a $ b => tryrules mem_pairs b
- | Const(\<^const_name>\<open>True\<close>,_) => []
- | Const(\<^const_name>\<open>False\<close>,_) => []
+ \<^Const_>\<open>mem for a b\<close> => tryrules mem_pairs b
+ | \<^Const_>\<open>True\<close> => []
+ | \<^Const_>\<open>False\<close> => []
| A => tryrules conn_pairs A)
| _ => [th]
end;