1.1 --- a/test/Tools/isac/Test_Some.thy	Thu Apr 05 16:44:21 2012 +0200
     1.2 +++ b/test/Tools/isac/Test_Some.thy	Thu Apr 05 16:53:43 2012 +0200
     1.3 @@ -33,11 +33,11 @@
     1.4  ML {*
     1.5  pbl_hierarchy2file (path ^ "pbl/");
     1.6  *}
     1.7 -text {*
     1.8 +ML {*
     1.9  pbls2file          (path ^ "pbl/");
    1.10  *}
    1.11  ML {*
    1.12 -str2term "inverse" (* = Const ("Rings.inverse_class.inverse", "RealDef.real \<Rightarrow> RealDef.real")*)
    1.13 +str2term "Inverse" (* = Const ("Rings.inverse_class.inverse", "RealDef.real \<Rightarrow> RealDef.real")*)
    1.14  *}
    1.15  ML {*
    1.16  met_hierarchy2file (path ^ "met/");