1.1 --- a/src/HOL/Statespace/state_space.ML	Sat Jan 15 22:40:17 2011 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Sun Jan 16 14:57:14 2011 +0100
     1.3 @@ -145,20 +145,20 @@
     1.4  
     1.5  fun prove_interpretation_in ctxt_tac (name, expr) thy =
     1.6     thy
     1.7 -   |> Expression.sublocale_cmd name expr []
     1.8 +   |> Expression.sublocale_cmd I name expr []
     1.9     |> Proof.global_terminal_proof
    1.10           (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    1.11     |> ProofContext.theory_of
    1.12  
    1.13  fun add_locale name expr elems thy =
    1.14    thy 
    1.15 -  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
    1.16 +  |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems
    1.17    |> snd
    1.18    |> Local_Theory.exit;
    1.19  
    1.20  fun add_locale_cmd name expr elems thy =
    1.21    thy 
    1.22 -  |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
    1.23 +  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
    1.24    |> snd
    1.25    |> Local_Theory.exit;
    1.26  
    1.27 @@ -349,7 +349,7 @@
    1.28  
    1.29  fun add_declaration name decl thy =
    1.30    thy
    1.31 -  |> Named_Target.init name
    1.32 +  |> Named_Target.init I name
    1.33    |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
    1.34    |> Local_Theory.exit_global;
    1.35