diff -r cd7854f2636d -r 02a9b2540eb7 src/Tools/isac/ProgLang/termC.sml
--- a/src/Tools/isac/ProgLang/termC.sml	Tue Sep 28 13:30:29 2010 +0200
+++ b/src/Tools/isac/ProgLang/termC.sml	Fri Oct 01 10:23:38 2010 +0200
@@ -1124,8 +1124,18 @@
 ***   Free ( R, RealDef.real)
 ***   Free ( R, RealDef.real)                  *)
 
+(*fun parse_patt thy str = 
+(**** prep_pbt: syntax error in '#Where' of ["equation"]
+*** Exception- TOPLEVEL_ERROR raised
+*** At command "ML" (line 172 of "/usr/local/isabisac/src/Tools/isac/Knowledge/Poly.thy").*)
+    (typ_a2real o numbers_to_string o
+     ProofContext.read_term_pattern (thy2ctxt thy)) str;*)
 fun parse_patt thy str = 
-    ProofContext.read_term_pattern (thy2ctxt thy) str;
+     ProofContext.read_term_pattern (thy2ctxt thy) str;
+(*fun parse_patt thy str = (thy, str) |>> thy2ctxt 
+                                    |-> ProofContext.read_term_pattern
+                                    |> numbers_to_string
+                                    |> typ_a2real;*)
 
 (*version for testing local to theories*)
 fun str2term_ thy str = (term_of o the o (parse thy)) str;