1.1 --- a/src/Tools/isac/ProgLang/termC.sml	Tue Sep 28 13:30:29 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Fri Oct 01 10:23:38 2010 +0200
     1.3 @@ -1124,8 +1124,18 @@
     1.4  ***   Free ( R, RealDef.real)
     1.5  ***   Free ( R, RealDef.real)                  *)
     1.6  
     1.7 +(*fun parse_patt thy str = 
     1.8 +(**** prep_pbt: syntax error in '#Where' of ["equation"]
     1.9 +*** Exception- TOPLEVEL_ERROR raised
    1.10 +*** At command "ML" (line 172 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Poly.thy").*)
    1.11 +    (typ_a2real o numbers_to_string o
    1.12 +     ProofContext.read_term_pattern (thy2ctxt thy)) str;*)
    1.13  fun parse_patt thy str = 
    1.14 -    ProofContext.read_term_pattern (thy2ctxt thy) str;
    1.15 +     ProofContext.read_term_pattern (thy2ctxt thy) str;
    1.16 +(*fun parse_patt thy str = (thy, str) |>> thy2ctxt 
    1.17 +                                    |-> ProofContext.read_term_pattern
    1.18 +                                    |> numbers_to_string
    1.19 +                                    |> typ_a2real;*)
    1.20  
    1.21  (*version for testing local to theories*)
    1.22  fun str2term_ thy str = (term_of o the o (parse thy)) str;