1.1 --- a/src/Tools/isac/ProgLang/termC.sml	Thu Nov 21 09:18:22 2013 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Thu Nov 21 11:17:42 2013 +0100
     1.3 @@ -738,10 +738,10 @@
     1.4    in assbl_thm sign_ref der maxidx shyps hyps (*tpairs*) prop' end;*)
     1.5  fun num_str thm =
     1.6    let val (deriv, 
     1.7 -	   {thy_ref = thy_ref, tags = tags, maxidx = maxidx, shyps = shyps, 
     1.8 +	   {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps, 
     1.9  	    hyps = hyps, tpairs = tpairs, prop = prop}) = rep_thm_G thm
    1.10      val prop' = numbers_to_string prop;
    1.11 -  in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;
    1.12 +  in assbl_thm deriv thy tags maxidx shyps hyps tpairs prop' end;
    1.13  
    1.14  fun get_thm' xstring = (*?covers 2009 Thm?!, replaces 2002 fun get_thm :
    1.15  val it = fn : theory -> xstring -> Thm.thm*)