--- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 26 14:27:46 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 26 14:43:56 2019 +0200
@@ -317,7 +317,7 @@
| make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
let val T = fastype_of1 (Ts, x)
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
- else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %>
+ else Proofterm.change_types (SOME [T]) subst_prf %> x %> y %>
Abs ("z", T, list_comb (incr_boundvars 1 f,
map (incr_boundvars 1) xs @ Bound 0 ::
map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
@@ -326,7 +326,7 @@
fun make_sym Ts ((x, y), (prf, clprf)) =
((y, x),
- (Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
+ (Proofterm.change_types (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
--- a/src/Pure/Proof/extraction.ML Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/extraction.ML Fri Jul 26 14:43:56 2019 +0200
@@ -116,7 +116,7 @@
in rew end;
-val chtype = Proofterm.change_type o SOME;
+val chtypes = Proofterm.change_types o SOME;
fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
fun corr_name s vs = extr_name s vs ^ "_correctness";
@@ -731,10 +731,10 @@
(Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
val corr_prf' = mkabsp shyps
- (chtype [] Proofterm.equal_elim_axm %> lhs %> rhs %%
- (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
- (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
- (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
+ (chtypes [] Proofterm.equal_elim_axm %> lhs %> rhs %%
+ (chtypes [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
+ (chtypes [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
+ (chtypes [T --> propT] Proofterm.reflexive_axm %> f) %%
PAxm (Thm.def_name cname, eqn,
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Reconstruct.prop_of corr_prf';
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 26 14:43:56 2019 +0200
@@ -243,7 +243,7 @@
(fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
map the ts);
in
- (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
+ (Proofterm.change_types (SOME [fastype_of1 (Ts, rhs')])
Proofterm.reflexive_axm %> rhs', true)
end
else (prf, false)
--- a/src/Pure/Proof/proof_syntax.ML Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Jul 26 14:43:56 2019 +0200
@@ -91,7 +91,7 @@
fun prf_of [] (Bound i) = PBound i
| prf_of Ts (Const (s, Type ("Pure.proof", _))) =
- Proofterm.change_type (if ty then SOME Ts else NONE)
+ Proofterm.change_types (if ty then SOME Ts else NONE)
(case Long_Name.explode s of
"axm" :: xs =>
let
@@ -111,7 +111,7 @@
| prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
(case try Logic.class_of_const c_class of
SOME c =>
- Proofterm.change_type (if ty then SOME Ts else NONE)
+ Proofterm.change_types (if ty then SOME Ts else NONE)
(OfClass (TVar ((Name.aT, 0), []), c))
| NONE => error ("Bad class constant: " ^ quote c_class))
| prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
--- a/src/Pure/Proof/reconstruct.ML Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML Fri Jul 26 14:43:56 2019 +0200
@@ -135,7 +135,7 @@
val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
(Proofterm.forall_intr_vfs prop) handle ListPair.UnequalLengths =>
error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
- in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
+ in (prop', Proofterm.change_types (SOME Ts) prf, [], env', vTs) end;
fun head_norm (prop, prf, cnstrts, env, vTs) =
(Envir.head_norm env prop, prf, cnstrts, env, vTs);
--- a/src/Pure/proofterm.ML Fri Jul 26 14:27:46 2019 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 26 14:43:56 2019 +0200
@@ -81,7 +81,7 @@
val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
val maxidx_proof: proof -> int -> int
val size_of_proof: proof -> int
- val change_type: typ list option -> proof -> proof
+ val change_types: typ list option -> proof -> proof
val prf_abstract_over: term -> proof -> proof
val prf_incr_bv: int -> int -> int -> int -> proof -> proof
val incr_pboundvars: int -> int -> proof -> proof
@@ -487,12 +487,12 @@
| size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
| size_of_proof _ = 1;
-fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs)
- | change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
- | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)
- | change_type opTs (PThm (i, ((name, prop, _, open_proof), body))) =
- PThm (i, ((name, prop, opTs, open_proof), body))
- | change_type _ prf = prf;
+fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
+ | change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c)
+ | change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
+ | change_types types (PThm (i, ((name, prop, _, open_proof), body))) =
+ PThm (i, ((name, prop, types, open_proof), body))
+ | change_types _ prf = prf;
(* utilities *)