src/Pure/deriv.ML
changeset 1601 0ef6ea27ab15
parent 1593 69ed69a9c32a
child 2042 33b4c1624e26
     1.1 --- a/src/Pure/deriv.ML	Thu Mar 21 11:13:05 1996 +0100
     1.2 +++ b/src/Pure/deriv.ML	Thu Mar 21 13:02:26 1996 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  		 | Asm of int
     1.5  		 | Res of deriv
     1.6  		 | Equal of deriv
     1.7 -		 | Thm   of theory * string
     1.8 +		 | Thm   of string
     1.9  		 | Other of deriv;
    1.10  
    1.11    val size : deriv -> int
    1.12 @@ -31,7 +31,7 @@
    1.13  (*Conversion to linear format.  Children of a node are the LIST of inferences
    1.14    justifying ONE of the premises*)
    1.15  fun rev_deriv (Join (rl, [])) 	= [Join(rl,[])]
    1.16 -  | rev_deriv (Join (Theorem arg, _)) 	= [Join(Theorem arg, [])]
    1.17 +  | rev_deriv (Join (Theorem name, _)) 	= [Join(Theorem name, [])]
    1.18    | rev_deriv (Join (Assumption arg, [der])) = 
    1.19                Join(Assumption arg,[]) :: rev_deriv der
    1.20    | rev_deriv (Join (Bicompose arg, [rder, sder])) =
    1.21 @@ -49,7 +49,7 @@
    1.22  	       | Asm of int
    1.23                 | Res of deriv
    1.24                 | Equal of deriv
    1.25 -               | Thm   of theory * string
    1.26 +               | Thm   of string
    1.27                 | Other of deriv;
    1.28  
    1.29  (*At position i, splice in value x, removing ngoal elements*)
    1.30 @@ -64,7 +64,7 @@
    1.31        simp_deriv der
    1.32    | simp_deriv (Join (Equal_elim, [Join (Reflexive _, []), der])) =
    1.33        simp_deriv der
    1.34 -  | simp_deriv (Join (rule as Theorem arg, [_])) = Join (rule, [])
    1.35 +  | simp_deriv (Join (rule as Theorem name, [_])) = Join (rule, [])
    1.36    | simp_deriv (Join (rule, ders)) = Join (rule, map simp_deriv ders);
    1.37  
    1.38  (*Proof term is an equality: first premise of equal_elim.
    1.39 @@ -132,7 +132,7 @@
    1.40  		       [rder, sder]), prfs) =
    1.41  		(*resolution with basic rule/assumption -- we hope!*)
    1.42        tree_aux (sder, splice (i, Res (simp_deriv rder), ngoal, prfs))
    1.43 -  | tree_aux (Join (Theorem arg, _), prfs)	= Join(Thm arg, prfs)
    1.44 +  | tree_aux (Join (Theorem name, _), prfs)	= Join(Thm name, prfs)
    1.45    | tree_aux (Join (_, [der]), prfs)	= tree_aux (der,prfs)
    1.46    | tree_aux (der, prfs) = Join(Other (simp_deriv der), prfs);
    1.47