test/Tools/isac/Specify/input-descript.sml
changeset 60309 70a1d102660d
parent 59959 0f0718c61f68
child 60336 dcb37736d573
     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";