src/HOL/Statespace/state_space.ML
changeset 33671 4b0f2599ed48
parent 33553 35f2b30593a8
child 36149 5ca66e58dcfa
     1.1 --- a/src/HOL/Statespace/state_space.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -155,13 +155,13 @@
     1.4    thy 
     1.5    |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
     1.6    |> snd
     1.7 -  |> LocalTheory.exit;
     1.8 +  |> Local_Theory.exit;
     1.9  
    1.10  fun add_locale_cmd name expr elems thy =
    1.11    thy 
    1.12    |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems
    1.13    |> snd
    1.14 -  |> LocalTheory.exit;
    1.15 +  |> Local_Theory.exit;
    1.16  
    1.17  type statespace_info =
    1.18   {args: (string * sort) list, (* type arguments *)
    1.19 @@ -350,8 +350,8 @@
    1.20  fun add_declaration name decl thy =
    1.21    thy
    1.22    |> Theory_Target.init name
    1.23 -  |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
    1.24 -  |> LocalTheory.exit_global;
    1.25 +  |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
    1.26 +  |> Local_Theory.exit_global;
    1.27  
    1.28  fun parent_components thy (Ts, pname, renaming) =
    1.29    let
    1.30 @@ -430,7 +430,7 @@
    1.31            let
    1.32              fun upd (n,v) =
    1.33                let
    1.34 -                val nT = ProofContext.infer_type (LocalTheory.target_of lthy) n
    1.35 +                val nT = ProofContext.infer_type (Local_Theory.target_of lthy) n
    1.36                in Context.proof_map
    1.37                    (update_declinfo (Morphism.term phi (Free (n,nT)),v))
    1.38                end;