1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri May 07 18:12:51 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -123,12 +123,15 @@
     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 Free (id, _)) =
     1.8 -    if TermC.is_num' id 
     1.9 -    then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
    1.10 +  | monom_of_term  vs (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
    1.11 +    if TermC.is_num t
    1.12 +    then (t |> HOLogic.dest_number |> snd |> string_of_int
    1.13 +      |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
    1.14      else (c, list_update es (find_index (curry op = t) vs) 1)
    1.15 -  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $ Free (e, _)) =
    1.16 -    (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
    1.17 +  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $
    1.18 +      (t as (Const ("Num.numeral_class.numeral", _) $ _)) $
    1.19 +        (Const ("Num.numeral_class.numeral", _) $ num)) =
    1.20 +    (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
    1.21    | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
    1.22      let val (c', es') = monom_of_term vs (c, es) m1
    1.23      in monom_of_term vs (c', es') m2 end
    1.24 @@ -179,7 +182,7 @@
    1.25    | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
    1.26    | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
    1.27    | term_of_es baseT expT (v :: vs) (e :: es) =
    1.28 -    Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $  (Free (TermC.isastr_of_int e, expT))
    1.29 +    Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
    1.30      :: term_of_es baseT expT vs es
    1.31    | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
    1.32  
    1.33 @@ -189,9 +192,10 @@
    1.34        if c = 1 
    1.35        then 
    1.36          if es' = [] (*if es = [0,0,0,...]*)
    1.37 -        then Free (TermC.isastr_of_int c, baseT)
    1.38 +        then HOLogic.mk_number baseT c
    1.39          else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
    1.40 -      else foldl (HOLogic.mk_binop "Groups.times_class.times") (Free (TermC.isastr_of_int c, baseT), es') 
    1.41 +      else foldl (HOLogic.mk_binop "Groups.times_class.times")
    1.42 +        (HOLogic.mk_number baseT c, es') 
    1.43      end
    1.44  
    1.45  fun term_of_poly baseT expT vs p =
    1.46 @@ -203,7 +207,7 @@
    1.47  ML \<open>
    1.48  fun mk_noteq_0 baseT t = 
    1.49    Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $ 
    1.50 -    (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
    1.51 +    (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
    1.52  
    1.53  fun mk_asms baseT ts =
    1.54    let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
    1.55 @@ -311,12 +315,12 @@
    1.56      (Const ("Groups.plus_class.plus", _) $ 
    1.57        nofrac $ 
    1.58        (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
    1.59 -    = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
    1.60 +    = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
    1.61    | check_frac_sum 
    1.62      (Const ("Groups.plus_class.plus", _) $ 
    1.63        (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $ 
    1.64        nofrac)
    1.65 -    = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
    1.66 +    = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
    1.67    | check_frac_sum _ = NONE  
    1.68  
    1.69  (* prepare a term for addition by providing the least common denominator as a product