# HG changeset patch
# User wenzelm
# Date 1226781080 -3600
# Node ID fc45401bdf6f28340126a17efd799f1a42857548
# Parent  48f7bfebd31d61f1eb8ed3fb1492b1ce0830d2b4
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
adapted PThm;

diff -r 48f7bfebd31d -r fc45401bdf6f src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Sat Nov 15 21:31:19 2008 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sat Nov 15 21:31:20 2008 +0100
@@ -16,7 +16,7 @@
 
 open Proofterm;
 
-val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) Symtab.empty true) o
+val rews = map (pairself (ProofSyntax.proof_of_term (the_context ()) true) o
     Logic.dest_equals o Logic.varify o ProofSyntax.read_term (the_context ()) propT)
 
   (** eliminate meta-equality rules **)
@@ -286,13 +286,13 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm ("HOL.cong", _, _, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %%
       prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
-  | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps)
+  | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
-val subst_prf = fst (strip_combt (Thm.proof_of subst));
-val sym_prf = fst (strip_combt (Thm.proof_of sym));
+val subst_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of subst)));
+val sym_prf = fst (strip_combt (Proofterm.proof_of (Thm.proof_of sym)));
 
 fun make_subst Ts prf xs (_, []) = prf
   | make_subst Ts prf xs (f, ((x, y), prf') :: ps) =
@@ -310,15 +310,15 @@
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
-fun elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % P % _ %% prf) =
+  | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (incr_pboundvars 1 0 prf))
-  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % _ %% prf1 %% prf2) =
+  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % P %% prf) =
+  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
   | elim_cong _ _ = NONE;