1.1 --- a/src/Tools/isac/Build_Isac.thy	Fri Sep 03 12:22:35 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Fri Sep 03 12:33:16 2010 +0200
     1.3 @@ -63,6 +63,15 @@
     1.4  use_thy "Knowledge/Atools"
     1.5  use_thy "Knowledge/Simplify"
     1.6  
     1.7 +ML {* print_depth 99;
     1.8 +val ctxt = ProofContext.init_global  @{theory};
     1.9 +ProofContext.read_term_pattern ctxt "matches (?a + ?b * bdv^2 = (0::real)) equ";
    1.10 +ProofContext.read_term_pattern ctxt "a + b * x^2 = (0::real)";
    1.11 +*}
    1.12 +
    1.13 +ML {* 
    1.14 +*}
    1.15 +
    1.16  use_thy "Knowledge/Poly"
    1.17  
    1.18