src/Pure/thm.ML
changeset 2047 a3701c4343ea
parent 2046 fd26cd4da8cf
child 2139 2c59b204b540
equal deleted inserted replaced
2046:fd26cd4da8cf 2047:a3701c4343ea
   361 
   361 
   362 datatype thm = Thm of
   362 datatype thm = Thm of
   363   {sign: Sign.sg,		(*signature for hyps and prop*)
   363   {sign: Sign.sg,		(*signature for hyps and prop*)
   364    der: deriv,			(*derivation*)
   364    der: deriv,			(*derivation*)
   365    maxidx: int,			(*maximum index of any Var or TVar*)
   365    maxidx: int,			(*maximum index of any Var or TVar*)
   366    shyps: sort list,		(* FIXME comment *)
   366    shyps: sort list,		(*sort hypotheses*)
   367    hyps: term list,		(*hypotheses*)
   367    hyps: term list,		(*hypotheses*)
   368    prop: term};			(*conclusion*)
   368    prop: term};			(*conclusion*)
   369 
   369 
   370 fun rep_thm (Thm args) = args;
   370 fun rep_thm (Thm args) = args;
   371 
   371