1.1 --- a/test/Tools/isac/Specify/input-descript.sml Mon Jun 21 14:39:52 2021 +0200
1.2 +++ b/test/Tools/isac/Specify/input-descript.sml Mon Jun 21 15:36:09 2021 +0200
1.3 @@ -16,7 +16,7 @@
1.4 "-------- distinguish input to I_Model --------------------------------------------------------";
1.5 "----- fun Input_Descript.for_bool_list -----";
1.6 val t as Const ("Input_Descript.relations",
1.7 - Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]),
1.8 + Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]),
1.9 Type ("Input_Descript.una", [])])) = @{term "relations"};
1.10 atomtyp (type_of t);
1.11 if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed";