1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri Sep 13 18:57:11 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Sep 16 10:46:51 2013 +0200
     1.3 @@ -112,7 +112,9 @@
     1.4        handle ERROR _ => NONE)
     1.5  
     1.6  fun is_poly t =
     1.7 -  let val vs = t |> vars |> map free2str |> sort string_ord
     1.8 +  let 
     1.9 +    val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
    1.10 +      |> filter is_some |> map the |> sort string_ord
    1.11    in 
    1.12      case poly_of_term vs t of SOME _ => true | NONE => false
    1.13    end
    1.14 @@ -310,7 +312,8 @@
    1.15        NONE => NONE
    1.16      | SOME (numerator, denominator) =>
    1.17        let 
    1.18 -        val vs = t |> vars |> map free2str |> sort string_ord
    1.19 +        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
    1.20 +          |> filter is_some |> map the |> sort string_ord
    1.21          val baseT = type_of numerator
    1.22          val expT = HOLogic.realT
    1.23        in
    1.24 @@ -353,7 +356,8 @@
    1.25        NONE => NONE
    1.26      | SOME (numerator, denominator) =>
    1.27        let 
    1.28 -        val vs = t |> vars |> map free2str |> sort string_ord
    1.29 +        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
    1.30 +          |> filter is_some |> map the |> sort string_ord
    1.31          val baseT = type_of numerator
    1.32          val expT = HOLogic.realT
    1.33        in
    1.34 @@ -405,7 +409,9 @@
    1.35      case opt of 
    1.36        NONE => NONE
    1.37      | SOME ((n1, d1), (n2, d2)) =>
    1.38 -      let val vs = t |> vars |> map free2str |> sort string_ord
    1.39 +      let 
    1.40 +        val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
    1.41 +          |> filter is_some |> map the |> sort string_ord
    1.42        in
    1.43          case (poly_of_term vs d1, poly_of_term vs d2) of
    1.44            (SOME a, SOME b) =>
    1.45 @@ -442,7 +448,8 @@
    1.46      NONE => NONE
    1.47    | SOME ((n1, d1), (n2, d2)) =>
    1.48      let 
    1.49 -      val vs = t |> vars |> map free2str |> sort string_ord
    1.50 +      val vs = t |> vars |> map str_of_free_opt (* tolerate Var in simplification *)
    1.51 +        |> filter is_some |> map the |> sort string_ord
    1.52      in
    1.53        case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
    1.54          (SOME _, SOME a, SOME _, SOME b) =>

     2.1 --- a/src/Tools/isac/ProgLang/termC.sml	Fri Sep 13 18:57:11 2013 +0200
     2.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Mon Sep 16 10:46:51 2013 +0200
     2.3 @@ -261,6 +261,8 @@
     2.4  
     2.5  fun free2str (Free (s,_)) = s
     2.6    | free2str t = error ("free2str not for "^ term2str t);
     2.7 +fun str_of_free_opt (Free (s,_)) = SOME s
     2.8 +  | str_of_free_opt _ = NONE
     2.9  fun free2int (t as Free (s, _)) = ((str2int s)
    2.10      handle _ => error ("free2int: "^term_detail2str t))
    2.11    | free2int t = error ("free2int: "^term_detail2str t);

     3.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Fri Sep 13 18:57:11 2013 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Mon Sep 16 10:46:51 2013 +0200
     3.3 @@ -322,9 +322,9 @@
     3.4  term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
     3.5    "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
     3.6  
     3.7 -val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
     3.8 -if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
     3.9 -else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
    3.10 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t''; 
    3.11 +if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then () 
    3.12 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; 
    3.13  
    3.14  (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
    3.15  val xxx = append_rls "multiply_ansatz_erls" norm_Rational