src/HOLCF/pcpodef_package.ML
changeset 18728 6790126ab5f6
parent 18678 dd0c569fa43d
child 18799 f137c5e971f5
     1.1 --- a/src/HOLCF/pcpodef_package.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOLCF/pcpodef_package.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -144,8 +144,9 @@
     1.4            ||> Theory.parent_path;
     1.5        in (theory', defs) end;
     1.6      
     1.7 -    fun pcpodef_result (theory, UUmem_admissible) =
     1.8 +    fun pcpodef_result (context, UUmem_admissible) =
     1.9        let
    1.10 +        val theory = Context.the_theory context;
    1.11          val UUmem = UUmem_admissible RS conjunct1;
    1.12          val admissible = UUmem_admissible RS conjunct2;
    1.13        in
    1.14 @@ -153,18 +154,19 @@
    1.15          |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
    1.16          |> make_cpo admissible
    1.17          |> make_pcpo UUmem
    1.18 -        |> (fn (theory', (type_def, _, _)) => (theory', type_def))
    1.19 +        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
    1.20        end;
    1.21    
    1.22 -    fun cpodef_result (theory, nonempty_admissible) =
    1.23 +    fun cpodef_result (context, nonempty_admissible) =
    1.24        let
    1.25 +        val theory = Context.the_theory context;
    1.26          val nonempty = nonempty_admissible RS conjunct1;
    1.27          val admissible = nonempty_admissible RS conjunct2;
    1.28        in
    1.29          theory
    1.30          |> make_po (Tactic.rtac nonempty 1)
    1.31          |> make_cpo admissible
    1.32 -        |> (fn (theory', (type_def, _, _)) => (theory', type_def))
    1.33 +        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
    1.34        end;
    1.35    
    1.36    in (goal, if pcpo then pcpodef_result else cpodef_result) end