src/Pure/proofterm.ML
changeset 16458 4c6fd0c01d28
parent 15797 a63605582573
child 16536 c5744af6b28a
     1.1 --- a/src/Pure/proofterm.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    val equal_elim : term -> term -> proof -> proof -> proof
     1.5    val axm_proof : string -> term -> proof
     1.6    val oracle_proof : string -> term -> proof
     1.7 -  val thm_proof : Sign.sg -> string * (string * string list) list ->
     1.8 +  val thm_proof : theory -> string * (string * string list) list ->
     1.9      term list -> term -> proof -> proof
    1.10    val get_name_tags : term list -> term -> proof -> string * (string * string list) list
    1.11  
    1.12 @@ -1093,21 +1093,19 @@
    1.13  
    1.14  (* data kind 'Pure/proof' *)
    1.15  
    1.16 -structure ProofArgs =
    1.17 -struct
    1.18 +structure ProofData = TheoryDataFun
    1.19 +(struct
    1.20    val name = "Pure/proof";
    1.21    type T = ((proof * proof) list *
    1.22      (string * (typ list -> proof -> proof option)) list);
    1.23  
    1.24    val empty = ([], []);
    1.25    val copy = I;
    1.26 -  val prep_ext = I;
    1.27 -  fun merge ((rules1, procs1), (rules2, procs2)) =
    1.28 +  val extend = I;
    1.29 +  fun merge _ ((rules1, procs1), (rules2, procs2)) =
    1.30      (merge_lists rules1 rules2, merge_alists procs1 procs2);
    1.31    fun print _ _ = ();
    1.32 -end;
    1.33 -
    1.34 -structure ProofData = TheoryDataFun(ProofArgs);
    1.35 +end);
    1.36  
    1.37  val init = ProofData.init;
    1.38  
    1.39 @@ -1119,7 +1117,7 @@
    1.40    let val r = ProofData.get thy
    1.41    in ProofData.put (fst r, ps @ snd r) thy end;
    1.42  
    1.43 -fun thm_proof sign (name, tags) hyps prop prf =
    1.44 +fun thm_proof thy (name, tags) hyps prop prf =
    1.45    let
    1.46      val prop = Logic.list_implies (hyps, prop);
    1.47      val nvs = needed_vars prop;
    1.48 @@ -1127,7 +1125,7 @@
    1.49          if ixn mem nvs then SOME v else NONE) (vars_of prop) @
    1.50        map SOME (sort (make_ord atless) (term_frees prop));
    1.51      val opt_prf = if ! proofs = 2 then
    1.52 -        #4 (shrink [] 0 (rewrite_prf fst (ProofData.get_sg sign)
    1.53 +        #4 (shrink [] 0 (rewrite_prf fst (ProofData.get thy)
    1.54            (foldr (uncurry implies_intr_proof) prf hyps)))
    1.55        else MinProof (mk_min_proof ([], prf));
    1.56      val head = (case strip_combt (fst (strip_combP prf)) of