src/Pure/deriv.ML

   (*Object-level rules*)
   datatype orule = Subgoal of cterm
 		 | Asm of int
 		 | Res of deriv
 		 | Equal of deriv
-		 | Thm   of theory * string
+		 | Thm   of string
 		 | Other of deriv;
 
   val size : deriv -> int
   val drop : 'a mtree * int -> 'a mtree
   val linear : deriv -> deriv list

   | size (Join(_, ders)) = foldl op+ (1, map size ders);
 
 (*Conversion to linear format.  Children of a node are the LIST of inferences
   justifying ONE of the premises*)
 fun rev_deriv (Join (rl, [])) 	= [Join(rl,[])]
-  | rev_deriv (Join (Theorem arg, _)) 	= [Join(Theorem arg, [])]
+  | rev_deriv (Join (Theorem name, _)) 	= [Join(Theorem name, [])]
   | rev_deriv (Join (Assumption arg, [der])) = 
               Join(Assumption arg,[]) :: rev_deriv der
   | rev_deriv (Join (Bicompose arg, [rder, sder])) =
 	Join (Bicompose arg, linear rder) :: rev_deriv sder
   | rev_deriv (Join (_, [der]))	= rev_deriv der

 (*Object-level rules*)
 datatype orule = Subgoal of cterm
 	       | Asm of int
                | Res of deriv
                | Equal of deriv
-               | Thm   of theory * string
+               | Thm   of string
                | Other of deriv;
 
 (*At position i, splice in value x, removing ngoal elements*)
 fun splice (i,x,ngoal,prfs) =
     let val prfs0 = take(i-1,prfs)

 (*Deletes trivial uses of Equal_elim; hides derivations of Theorems*)
 fun simp_deriv (Join (Equal_elim, [Join (Rewrite_cterm _, []), der])) =
       simp_deriv der
   | simp_deriv (Join (Equal_elim, [Join (Reflexive _, []), der])) =
       simp_deriv der
-  | simp_deriv (Join (rule as Theorem arg, [_])) = Join (rule, [])
+  | simp_deriv (Join (rule as Theorem name, [_])) = Join (rule, [])
   | simp_deriv (Join (rule, ders)) = Join (rule, map simp_deriv ders);
 
 (*Proof term is an equality: first premise of equal_elim.
   Attempt to decode proof terms made by Drule.goals_conv.
   Subgoal numbers are returned; they are wrong if original subgoal

 				[der2, der3])]), prfs)
   | tree_aux (Join (Bicompose (arg as (_,_,i,ngoal,_)), 
 		       [rder, sder]), prfs) =
 		(*resolution with basic rule/assumption -- we hope!*)
       tree_aux (sder, splice (i, Res (simp_deriv rder), ngoal, prfs))
-  | tree_aux (Join (Theorem arg, _), prfs)	= Join(Thm arg, prfs)
+  | tree_aux (Join (Theorem name, _), prfs)	= Join(Thm name, prfs)
   | tree_aux (Join (_, [der]), prfs)	= tree_aux (der,prfs)
   | tree_aux (der, prfs) = Join(Other (simp_deriv der), prfs);
 
 
 fun tree der = tree_aux (der,[]);