1.1 --- a/test/Tools/isac/ProgLang/termC.sml	Mon Sep 02 15:17:34 2013 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/termC.sml	Mon Sep 02 16:16:08 2013 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4   val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
     1.5   (*        !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
     1.6   val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
     1.7 -print_depth 999; insts; 
     1.8 +print_depth 3; (*999*) insts; 
     1.9   (*val insts =
    1.10     ({}, 
    1.11      {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))),