1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sat Jul 03 16:21:07 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jul 12 17:21:37 2021 +0200
     1.3 @@ -123,14 +123,18 @@
     1.4  ML \<open>
     1.5  fun monom_of_term vs (c, es) (t as Const _) =
     1.6      (c, list_update es (find_index (curry op = t) vs) 1)
     1.7 -  | monom_of_term vs (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
     1.8 -    (t |> HOLogic.dest_number |> snd |> string_of_int
     1.9 -      |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
    1.10 +  | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
    1.11 +    (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
    1.12 +  | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
    1.13 +    (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
    1.14    | monom_of_term  vs (c, es) (t as Free _) =
    1.15      (c, list_update es (find_index (curry op = t) vs) 1)
    1.16 -  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $
    1.17 -      (Const ("Num.numeral_class.numeral", _) $ num)) =
    1.18 -    (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
    1.19 +  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
    1.20 +      (e as Const ("Num.numeral_class.numeral", _) $ _)) =
    1.21 +    (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    1.22 +  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
    1.23 +      (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
    1.24 +    (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
    1.25    | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
    1.26      let val (c', es') = monom_of_term vs (c, es) m1
    1.27      in monom_of_term vs (c', es') m2 end
    1.28 @@ -139,6 +143,10 @@
    1.29  (*-------v------*)
    1.30  fun monoms_of_term vs (t as Const _) =
    1.31      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.32 +  | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
    1.33 +    [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.34 +  | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
    1.35 +    [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.36    | monoms_of_term vs (t as Free _) =
    1.37      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.38    | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $  _) =