# HG changeset patch
# User wenzelm
# Date 877513003 -7200
# Node ID e1843233c694f207368e07729c85baf779a17c4b
# Parent  9c742951a923f2a333dbefa094e7fa4a131d5d52
tuned;

diff -r 9c742951a923 -r e1843233c694 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 22 11:36:29 1997 +0200
+++ b/src/Pure/thm.ML	Wed Oct 22 11:36:43 1997 +0200
@@ -180,7 +180,6 @@
 
 datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
 
-(* FIXME tune!? *)
 fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
 fun typ_of (Ctyp {T, ...}) = T;
 
@@ -198,7 +197,6 @@
 
 datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
 
-(* FIXME tune!? *)
 fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
 
@@ -396,7 +394,6 @@
   hyps: term list,             (*hypotheses*)
   prop: term};                 (*conclusion*)
 
-(* FIXME tune!? *)
 fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
   {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
     shyps = shyps, hyps = hyps, prop = prop};