1.1 --- a/src/Pure/proofterm.ML	Tue Sep 23 15:48:50 2008 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Sep 23 15:48:51 2008 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4    val mk_min_proof : proof ->
     1.5     ((string * term) * proof) list * (string * term) list * (string * term) list ->
     1.6     ((string * term) * proof) list * (string * term) list * (string * term) list
     1.7 -  val oracles_of_proof : proof -> (string * term) list -> (string * term) list
     1.8 +  val add_oracles : bool -> proof -> (string * term) list -> (string * term) list
     1.9  
    1.10    (** proof terms for specific inference rules **)
    1.11    val implies_intr_proof : term -> proof -> proof
    1.12 @@ -104,7 +104,6 @@
    1.13    val promise_proof : serial -> term -> proof
    1.14    val thm_proof : theory -> string -> term list -> term -> proof -> proof
    1.15    val get_name : term list -> term -> proof -> string
    1.16 -  val is_named : proof -> bool
    1.17  
    1.18    (** rewriting on proof terms **)
    1.19    val add_prf_rrule : proof * proof -> theory -> theory
    1.20 @@ -115,6 +114,7 @@
    1.21    val rewrite_proof_notypes : (proof * proof) list *
    1.22      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    1.23    val rew_proof : theory -> proof -> proof
    1.24 +  val fulfill : proof Inttab.table -> proof -> proof
    1.25  end
    1.26  
    1.27  structure Proofterm : PROOFTERM =
    1.28 @@ -147,10 +147,8 @@
    1.29        | oras_of (prf % _) = oras_of prf
    1.30        | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
    1.31        | oras_of (PThm (name, prf, prop, _)) = (fn tabs as (thms, oras) =>
    1.32 -          case Symtab.lookup thms name of
    1.33 -            NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras)
    1.34 -          | SOME ps => if member (op =) ps prop then tabs else
    1.35 -              oras_of prf (Symtab.update (name, prop::ps) thms, oras))
    1.36 +          if member (op =) (Symtab.lookup_list thms name) prop then tabs
    1.37 +          else oras_of prf (Symtab.cons_list (name, prop) thms, oras))
    1.38        | oras_of (Oracle (s, prop, _)) =
    1.39            apsnd (OrdList.insert string_term_ord (s, prop))
    1.40        | oras_of (MinProof (thms, _, oras)) =
    1.41 @@ -161,15 +159,16 @@
    1.42      snd (oras_of prf (Symtab.empty, oras))
    1.43    end;
    1.44  
    1.45 +fun add_oracles false = K I
    1.46 +  | add_oracles true = oracles_of_proof;
    1.47 +
    1.48  fun thms_of_proof (Abst (_, _, prf)) = thms_of_proof prf
    1.49    | thms_of_proof (AbsP (_, _, prf)) = thms_of_proof prf
    1.50    | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
    1.51    | thms_of_proof (prf % _) = thms_of_proof prf
    1.52    | thms_of_proof (prf' as PThm (s, prf, prop, _)) = (fn tab =>
    1.53 -      case Symtab.lookup tab s of
    1.54 -        NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab)
    1.55 -      | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
    1.56 -          thms_of_proof prf (Symtab.update (s, (prop, prf')::ps) tab))
    1.57 +      if exists (fn (p, _) => p = prop) (Symtab.lookup_list tab s) then tab
    1.58 +      else thms_of_proof prf (Symtab.cons_list (s, (prop, prf')) tab))
    1.59    | thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
    1.60    | thms_of_proof _ = I;
    1.61  
    1.62 @@ -179,11 +178,8 @@
    1.63    | thms_of_proof' (prf1 %% prf2) = thms_of_proof' prf1 #> thms_of_proof' prf2
    1.64    | thms_of_proof' (prf % _) = thms_of_proof' prf
    1.65    | thms_of_proof' (PThm ("", prf, prop, _)) = thms_of_proof' prf
    1.66 -  | thms_of_proof' (prf' as PThm (s, _, prop, _)) = (fn tab =>
    1.67 -      case Symtab.lookup tab s of
    1.68 -        NONE => Symtab.update (s, [(prop, prf')]) tab
    1.69 -      | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
    1.70 -          Symtab.update (s, (prop, prf')::ps) tab)
    1.71 +  | thms_of_proof' (prf' as PThm (s, _, prop, _)) =
    1.72 +      Symtab.insert_list (eq_fst op =) (s, (prop, prf'))
    1.73    | thms_of_proof' (MinProof (prfs, _, _)) = fold (thms_of_proof' o proof_of_min_thm) prfs
    1.74    | thms_of_proof' _ = I;
    1.75  
    1.76 @@ -1088,6 +1084,7 @@
    1.77        | _ => false
    1.78    end;
    1.79  
    1.80 +
    1.81  (**** rewriting on proof terms ****)
    1.82  
    1.83  val skel0 = PBound 0;
    1.84 @@ -1165,6 +1162,9 @@
    1.85  
    1.86  fun rewrite_proof_notypes rews = rewrite_prf fst rews;
    1.87  
    1.88 +fun fulfill tab = rewrite_proof_notypes
    1.89 +  ([], [("Pure/fulfill", K (fn Promise (i, _, _) => Inttab.lookup tab i | _ => NONE))]);
    1.90 +
    1.91  
    1.92  (**** theory data ****)
    1.93  
    1.94 @@ -1217,10 +1217,6 @@
    1.95      | _ => "")
    1.96    end;
    1.97  
    1.98 -fun is_named (PThm (name, _, _, _)) = name <> ""
    1.99 -  | is_named (PAxm (name, _, _)) = name <> ""
   1.100 -  | is_named _ = false;
   1.101 -
   1.102  end;
   1.103  
   1.104  structure BasicProofterm : BASIC_PROOFTERM = Proofterm;