src/HOL/Statespace/state_space.ML

--- a/src/HOL/Statespace/state_space.ML	Sat Jan 15 22:40:17 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sun Jan 16 14:57:14 2011 +0100
@@ -145,20 +145,20 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Expression.sublocale_cmd name expr []
+   |> Expression.sublocale_cmd I name expr []
    |> Proof.global_terminal_proof
          (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> ProofContext.theory_of
 
 fun add_locale name expr elems thy =
   thy 
-  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
+  |> Expression.add_locale I (Binding.name name) (Binding.name name) expr elems
   |> snd
   |> Local_Theory.exit;
 
 fun add_locale_cmd name expr elems thy =
   thy 
-  |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
+  |> Expression.add_locale_cmd I (Binding.name name) Binding.empty expr elems
   |> snd
   |> Local_Theory.exit;
 
@@ -349,7 +349,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init name
+  |> Named_Target.init I name
   |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
   |> Local_Theory.exit_global;