test/Tools/isac/BaseDefinitions/substitution.sml
changeset 60336 dcb37736d573
parent 60331 40eb8aa2b0d6
child 60500 59a3af532717
     1.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -74,9 +74,9 @@
     1.4    [(Free ("bdv_1", _), Free ("x", _)),
     1.5     (Free ("bdv_2", _), Free ("y", _)),
     1.6      (Free ("xxx", _),
     1.7 -     Const ("Groups.plus_class.plus", _) $ Free ("aaa", _) $
     1.8 -       (Const ("Num.numeral_class.numeral", _) $
     1.9 -         (Const ("Num.num.Bit1", _) $ _ )))] => ()
    1.10 +     Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Free ("aaa", _) $
    1.11 +       (Const (\<^const_name>\<open>numeral\<close>, _) $
    1.12 +         (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ _ )))] => ()
    1.13  | _ => error "fun T_from_string_eqs";
    1.14  
    1.15  "-------- fun input_to_terms -------------------------------------------------";
    1.16 @@ -87,7 +87,7 @@
    1.17  
    1.18  case Subst.input_to_terms input of
    1.19    [Const (\<^const_name>\<open>Pair\<close>, _) $
    1.20 -    (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const ("String.char.Char", _) $
    1.21 +    (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Char\<close>, _) $
    1.22        Const (\<^const_name>\<open>False\<close>, _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $
    1.23      Free ("x", _),
    1.24    _,