# HG changeset patch
# User huffman
# Date 1240337464 25200
# Node ID 21ce52733a4d9c9d5264c4b40ca58ef5b4d3d9f9
# Parent  182fa14e1844ad7e472d0dbb1de489a5159076f9
use Sign.add_consts instead of ContConsts.add_consts

diff -r 182fa14e1844 -r 21ce52733a4d src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Apr 21 06:44:14 2009 -0700
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Apr 21 11:11:04 2009 -0700
@@ -347,12 +347,12 @@
 val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list 
 							atyp statetupel trans;
 val thy2 = (thy
-|> ContConsts.add_consts
-[(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn),
-(automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn),
-(automaton_name ^ "_trans",
+|> Sign.add_consts
+[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn),
+(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn),
+(Binding.name (automaton_name ^ "_trans"),
  "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
-(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
+(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
 |> add_defs
 [(automaton_name ^ "_initial_def",
 automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
@@ -386,8 +386,8 @@
 val comp_list = clist aut_list;
 in
 thy
-|> ContConsts.add_consts_i
-[(automaton_name,
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
 Type("*",
 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
  Type("*",[Type("set",[st_typ]),
@@ -407,8 +407,8 @@
 val rest_set = action_set_string thy acttyp actlist
 in
 thy
-|> ContConsts.add_consts_i
-[(automaton_name, auttyp,NoSyn)]
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
 |> add_defs
 [(automaton_name ^ "_def",
 automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
@@ -421,8 +421,8 @@
 val hid_set = action_set_string thy acttyp actlist
 in
 thy
-|> ContConsts.add_consts_i
-[(automaton_name, auttyp,NoSyn)]
+|> Sign.add_consts_i
+[(Binding.name automaton_name, auttyp,NoSyn)]
 |> add_defs
 [(automaton_name ^ "_def",
 automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
@@ -441,8 +441,8 @@
 val acttyp = ren_act_type_of thy fun_name
 in
 thy
-|> ContConsts.add_consts_i
-[(automaton_name,
+|> Sign.add_consts_i
+[(Binding.name automaton_name,
 Type("*",
 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
  Type("*",[Type("set",[st_typ]),