src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 26603 410d02ea13c9
parent 26552 5677b4faf295
child 26613 725a3d9011d1
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 13:24:19 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 10 13:24:20 2008 +0200
     1.3 @@ -485,7 +485,7 @@
     1.4      s |> OuterSyntax.scan |> OuterSyntax.read
     1.5        (*|> map (Toplevel.position Position.none o #3)*)
     1.6        |> map #3
     1.7 -      |> Toplevel.>>>;
     1.8 +      |> Isar.>>>;
     1.9  
    1.10  (* TODO:
    1.11      - apply a command given a transition function, e.g. IsarCmd.undo.
    1.12 @@ -710,7 +710,7 @@
    1.13              let
    1.14                  (* TODO: interim: this is probably not right.
    1.15                     What we want is mapping onto simple PGIP name/context model. *)
    1.16 -                val ctx = Toplevel.context_of (Toplevel.get_state()) (* NB: raises UNDEF *)
    1.17 +                val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *)
    1.18                  val thy = Context.theory_of_proof ctx
    1.19                  val ths = [PureThy.get_thm thy thmname]
    1.20                  val deps = filter_out (equal "")
    1.21 @@ -739,7 +739,7 @@
    1.22          val objtype = #objtype vs
    1.23          val name = #name vs
    1.24  
    1.25 -        val topthy = Toplevel.theory_of o Toplevel.get_state
    1.26 +        val topthy = Toplevel.theory_of o Isar.state
    1.27  
    1.28          fun splitthy id =
    1.29              let val comps = NameSpace.explode id
    1.30 @@ -796,7 +796,7 @@
    1.31      let
    1.32          val openfile = !currently_open_file
    1.33  
    1.34 -        val topthy = Toplevel.theory_of o Toplevel.get_state
    1.35 +        val topthy = Toplevel.theory_of o Isar.state
    1.36          val topthy_name = Context.theory_name o topthy
    1.37  
    1.38          val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE