src/HOL/Tools/Function/size.ML
changeset 33766 c679f05600cd
parent 33671 4b0f2599ed48
child 33968 f94fb13ecbb3
     1.1 --- a/src/HOL/Tools/Function/size.ML	Thu Nov 19 14:45:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Nov 19 14:46:33 2009 +0100
     1.3 @@ -130,8 +130,8 @@
     1.4      fun define_overloaded (def_name, eq) lthy =
     1.5        let
     1.6          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
     1.7 -        val ((_, (_, thm)), lthy') = lthy |> Local_Theory.define Thm.definitionK
     1.8 -          ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
     1.9 +        val ((_, (_, thm)), lthy') = lthy
    1.10 +          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
    1.11          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
    1.12          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
    1.13        in (thm', lthy') end;