# HG changeset patch # User wenzelm # Date 1564145036 -7200 # Node ID eb6ff14767cd28679a7d2a899df47de628e3eb24 # Parent 5be1da847b24f57a97b0811ee7a81cccd36d4d2a tuned signature; diff -r 5be1da847b24 -r eb6ff14767cd src/HOL/Tools/rewrite_hol_proof.ML --- 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); diff -r 5be1da847b24 -r eb6ff14767cd src/Pure/Proof/extraction.ML --- 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'; diff -r 5be1da847b24 -r eb6ff14767cd src/Pure/Proof/proof_rewrite_rules.ML --- 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) diff -r 5be1da847b24 -r eb6ff14767cd src/Pure/Proof/proof_syntax.ML --- 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 diff -r 5be1da847b24 -r eb6ff14767cd src/Pure/Proof/reconstruct.ML --- 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); diff -r 5be1da847b24 -r eb6ff14767cd src/Pure/proofterm.ML --- 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 *)