1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Mon Jul 25 14:19:50 2011 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Tue Jul 26 09:09:49 2011 +0200
     1.3 @@ -23,13 +23,13 @@
     1.4  "--------------------------------------------------------";
     1.5  "--------------------------------------------------------";
     1.6  
     1.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     1.8  
     1.9  "----------- assemble rewrite ---------------------------";
    1.10  "----------- assemble rewrite ---------------------------";
    1.11  "----------- assemble rewrite ---------------------------";
    1.12  "===== rewriting by thm with 'a";
    1.13  (*show_types := true;*)
    1.14 +
    1.15  val thy = @{theory Complex_Main};
    1.16  val ctxt = @{context};
    1.17  val thm = @{thm add_commute};
    1.18 @@ -73,7 +73,7 @@
    1.19  (*is displayed on top of <response> buffer...*)
    1.20  Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r');
    1.21  Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
    1.22 -(*}*)
    1.23 +(**)
    1.24  
    1.25  "----------- test rewriting without Isac's thys ---------";
    1.26  "----------- test rewriting without Isac's thys ---------";
    1.27 @@ -347,7 +347,6 @@
    1.28  imports Main Complex
    1.29  begin
    1.30  
    1.31 -ML {*
    1.32  let
    1.33    val parser = Args.context -- Scan.lift Args.name_source
    1.34    fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt
    1.35 @@ -355,20 +354,17 @@
    1.36  in
    1.37    ML_Antiquote.inline "term_pat" (parser >> term_pat)
    1.38  end
    1.39 -*}
    1.40  
    1.41 -ML {*
    1.42    val t = @{term "a + b * x = (0 ::real)"};
    1.43    val pat = @{term_pat "?l = (?r ::real)"};
    1.44    val precond = @{term_pat "is_polynomial (?l::real)"};
    1.45    val inst = Pattern.match @{theory} (pat, t) (Vartab.empty, Vartab.empty);
    1.46 -*}
    1.47  
    1.48 -ML {*
    1.49    Envir.subst_term inst precond
    1.50    |> Syntax.string_of_term @{context}
    1.51    |> writeln
    1.52 -*}
    1.53 +
    1.54 +
    1.55  end *)
    1.56  val thy = @{theory "Isac"};
    1.57  val t = @{term "a + b * x = (0 ::real)"};
    1.58 @@ -522,5 +518,3 @@
    1.59  case eval__true thy i asms bdv rls of 
    1.60      ([], true) => ()
    1.61    | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
    1.62 -
    1.63 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)