src/HOL/HOLCF/Tools/Domain/domain_induction.ML
changeset 42375 774df7c59508
parent 42364 8c674b3b8e44
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 13:47:22 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 19:54:04 2011 +0200
     1.3 @@ -264,7 +264,7 @@
     1.4    val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
     1.5    val bisim_type = R_types ---> boolT
     1.6    val (bisim_const, thy) =
     1.7 -      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy
     1.8 +      Sign.declare_const_global ((bisim_bind, bisim_type), NoSyn) thy
     1.9  
    1.10    (* define bisimulation predicate *)
    1.11    local