1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Fri Oct 12 16:03:07 2012 +0200
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Fri Oct 12 17:06:58 2012 +0200
     1.3 @@ -1736,7 +1736,7 @@
     1.4      val thy = assoc_thy dI;
     1.5  	  val {ppc, ...} = get_met mI;
     1.6      val (fmz_, vals) = oris2fmz_vals pors;
     1.7 -	  val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global 
     1.8 +	  val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global 
     1.9        |> declare_constraints' vals
    1.10      val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
    1.11  	  val pt = update_metppc pt p (map (ori2Coritm ppc) pors); (*WN110716 = _pblppc ?!?*)