ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
authorwenzelm
Sat Nov 15 21:31:20 2008 +0100 (2008-11-15)
changeset 28801fc45401bdf6f
parent 28800 48f7bfebd31d
child 28802 9ba30eeec7ce
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
adapted PThm;
src/HOL/Tools/rewrite_hol_proof.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Sat Nov 15 21:31:19 2008 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sat Nov 15 21:31:20 2008 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  open Proofterm;
     1.6  
     1.7 -val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
     1.8 +val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
     1.9      Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
    1.10  
    1.11    (** eliminate meta-equality rules **)
    1.12 @@ -286,13 +286,13 @@
    1.13  
    1.14  (** Replace congruence rules by substitution rules **)
    1.15  
    1.16 -fun strip_cong ps (PThm ("HOL.cong", _, _, _) % _ % _ % SOME x % SOME y %%
    1.17 +fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
    1.18        prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
    1.19 -  | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps)
    1.20 +  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
    1.21    | strip_cong _ _ = NONE;
    1.22  
    1.23 -val subst_prf = fst (strip_combt (Thm.proof_of subst));
    1.24 -val sym_prf = fst (strip_combt (Thm.proof_of sym));
    1.25 +val subst_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of subst)));
    1.26 +val sym_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of sym)));
    1.27  
    1.28  fun make_subst Ts prf xs (_, []) = prf
    1.29    | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
    1.30 @@ -310,15 +310,15 @@
    1.31  
    1.32  fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
    1.33  
    1.34 -fun elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % _ % _ %% prf1 %% prf2) =
    1.35 +fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
    1.36        Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
    1.37 -  | elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % P % _ %% prf) =
    1.38 +  | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
    1.39        Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
    1.40          (strip_cong [] (incr_pboundvars 1 0 prf))
    1.41 -  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % _ %% prf1 %% prf2) =
    1.42 +  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
    1.43        Option.map (make_subst Ts prf2 [] o
    1.44          apsnd (map (make_sym Ts))) (strip_cong [] prf1)
    1.45 -  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % P %% prf) =
    1.46 +  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
    1.47        Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
    1.48          apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
    1.49    | elim_cong _ _ = NONE;