src/HOL/Tools/Function/fun.ML
changeset 33671 4b0f2599ed48
parent 33171 292970b42770
child 33726 0878aecbf119
     1.1 --- a/src/HOL/Tools/Function/fun.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/fun.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -153,11 +153,11 @@
     1.4  fun gen_fun add config fixes statements int lthy =
     1.5    let val group = serial () in
     1.6      lthy
     1.7 -      |> LocalTheory.set_group group
     1.8 +      |> Local_Theory.set_group group
     1.9        |> add fixes statements config
    1.10        |> by_pat_completeness_auto int
    1.11 -      |> LocalTheory.restore
    1.12 -      |> LocalTheory.set_group group
    1.13 +      |> Local_Theory.restore
    1.14 +      |> Local_Theory.set_group group
    1.15        |> termination_by (Function_Common.get_termination_prover lthy) int
    1.16    end;
    1.17