src/HOL/Tools/function_package/fundef_package.ML
changeset 24508 c8b82fec6447
parent 24168 86a03a092062
child 24624 b8383b1bbae3
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Sep 01 01:22:11 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Sep 01 15:46:59 2007 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  fun setup_termination_proof term_opt lthy =
     1.5      let
     1.6        val data = the (case term_opt of
     1.7 -                        SOME t => import_fundef_data (ProofContext.read_term lthy t) (Context.Proof lthy)
     1.8 +                        SOME t => import_fundef_data (Syntax.read_term lthy t) (Context.Proof lthy)
     1.9                        | NONE => import_last_fundef (Context.Proof lthy))
    1.10            handle Option.Option => raise ERROR ("Not a function: " ^ quote (the_default "" term_opt))
    1.11