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) =>