src/HOL/Statespace/state_space.ML
changeset 30346 90efbb8a8cb2
parent 30289 b28caca9157f
child 30364 577edc39b501
     1.1 --- a/src/HOL/Statespace/state_space.ML	Sat Mar 07 22:17:25 2009 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Mar 07 23:30:58 2009 +0100
     1.3 @@ -154,13 +154,13 @@
     1.4  
     1.5  fun add_locale name expr elems thy =
     1.6    thy 
     1.7 -  |> Expression.add_locale name name expr elems
     1.8 +  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
     1.9    |> snd
    1.10    |> LocalTheory.exit;
    1.11  
    1.12  fun add_locale_cmd name expr elems thy =
    1.13    thy 
    1.14 -  |> Expression.add_locale_cmd name "" expr elems
    1.15 +  |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
    1.16    |> snd
    1.17    |> LocalTheory.exit;
    1.18