1.1 --- a/src/Pure/thm.ML	Sat Dec 05 16:09:41 2015 +0100
     1.2 +++ b/src/Pure/thm.ML	Sun Dec 06 08:45:16 2015 +0100
     1.3 @@ -57,6 +57,16 @@
     1.4      hyps: term Ord_List.T,
     1.5      tpairs: (term * term) list,
     1.6      prop: term}
     1.7 +  type deriv (*WN*)
     1.8 +  val rep_thm_G:(*WN*) thm ->
     1.9 +   deriv *
    1.10 +   {thy: theory,               (*new since 2002, updated 2013-1*)
    1.11 +    tags: Properties.T,        (*new since 2002*)
    1.12 +    maxidx: int,
    1.13 +    shyps: sort Ord_List.T,
    1.14 +    hyps: term Ord_List.T,
    1.15 +    tpairs: (term * term) list,(*new since 2002*)
    1.16 +    prop: term}
    1.17    val crep_thm: thm ->
    1.18     {thy: theory,
    1.19      tags: Properties.T,
    1.20 @@ -81,6 +91,16 @@
    1.21    val major_prem_of: thm -> term
    1.22    val cprop_of: thm -> cterm
    1.23    val cprem_of: thm -> int -> cterm
    1.24 +  val make_thm:(*WN*) cterm -> thm
    1.25 +  val assbl_thm:(*WN*) deriv -> 
    1.26 +		       theory -> 
    1.27 +		       Properties.T -> 
    1.28 +		       int -> 
    1.29 +		       sort Ord_List.T -> 
    1.30 +		       term Ord_List.T ->
    1.31 +		       (term * term) list ->
    1.32 +		       term ->
    1.33 +		       thm
    1.34    val transfer: theory -> thm -> thm
    1.35    val renamed_prop: term -> thm -> thm
    1.36    val weaken: cterm -> thm -> thm
    1.37 @@ -339,6 +359,7 @@
    1.38  exception THM of string * int * thm list;
    1.39  
    1.40  fun rep_thm (Thm (_, args)) = args;
    1.41 +fun rep_thm_G (Thm (deriv , args)) = (deriv, args); (*WN*)
    1.42  
    1.43  fun crep_thm (Thm (_, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
    1.44    let fun cterm max t = Cterm {thy = thy, t = t, T = propT, maxidx = max, sorts = shyps} in
    1.45 @@ -668,6 +689,24 @@
    1.46        tpairs = [],
    1.47        prop = prop})
    1.48    end;
    1.49 +fun make_thm raw_ct =                                     (*WN  ---vvv *)
    1.50 +  let val Cterm {thy, t = prop, T, maxidx, sorts} = adjust_maxidx_cterm ~1 raw_ct in
    1.51 +    if T <> propT then
    1.52 +      raise THM ("make_thm: prop", 0, [])
    1.53 +  (*else if maxidx <> ~1 then (*WN true with matches (?b * v_ = 0)..*)
    1.54 +      raise THM ("make_thm: variables", maxidx, [])*)
    1.55 +    else Thm (deriv_rule0 (Proofterm.Hyp prop),
    1.56 +	      {thy = thy,
    1.57 +	       tags = [],
    1.58 +	       maxidx = ~1,
    1.59 +	       shyps = sorts,
    1.60 +	       hyps = [prop],
    1.61 +	       tpairs = [],
    1.62 +	       prop = prop})
    1.63 +  end;
    1.64 +fun assbl_thm deriv thy tags maxidx shyps hyps tpairs prop = (*WN*)
    1.65 +    Thm (deriv, {thy=thy, tags=tags, maxidx=maxidx,
    1.66 +	shyps=shyps, hyps=hyps, tpairs=tpairs, prop=prop});     (*WN  ---^^^ *)
    1.67  
    1.68  (*Implication introduction
    1.69      [A]