1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri May 20 07:24:18 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri May 20 08:12:51 2011 +0200
     1.3 @@ -1534,7 +1534,7 @@
     1.4  		          (hd o #met o get_pbt) pI') end
     1.5  	        else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
     1.6  	      val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
     1.7 -	      val dI = theory2theory' (maxthy thy thy');
     1.8 +	      val dI = theory2theory' (maxthy thy thy')
     1.9  	      val hdl = 
    1.10            case cas of
    1.11  		        NONE => pblterm dI pI