src/Pure/Isar/local_defs.ML
changeset 24261 dd31811bdf46
parent 24039 273698405054
child 24961 5298ee9c3fe5
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Aug 14 13:20:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Aug 14 13:20:19 2007 +0200
     1.3 @@ -45,11 +45,11 @@
     1.4      fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
     1.5      val ((lhs, _), eq') = eq
     1.6        |> Sign.no_vars pp
     1.7 -      |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
     1.8 +      |> PrimitiveDefs.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
     1.9        handle TERM (msg, _) => err msg | ERROR msg => err msg;
    1.10    in (Term.dest_Free (Term.head_of lhs), eq') end;
    1.11  
    1.12 -val abs_def = Logic.abs_def #>> Term.dest_Free;
    1.13 +val abs_def = PrimitiveDefs.abs_def #>> Term.dest_Free;
    1.14  
    1.15  fun mk_def ctxt args =
    1.16    let