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 _,