src/Pure/sign.ML
changeset 33385 fb2358edcfb6
parent 33173 b8ca12f6681a
child 33724 5ee13e0428d2
     1.1 --- a/src/Pure/sign.ML	Mon Nov 02 20:34:59 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Nov 02 20:38:46 2009 +0100
     1.3 @@ -392,7 +392,7 @@
     1.4    let val ((lhs, rhs), _) = tm
     1.5      |> no_vars (Syntax.pp ctxt)
     1.6      |> Logic.strip_imp_concl
     1.7 -    |> PrimitiveDefs.dest_def ctxt Term.is_Const (K false) (K false)
     1.8 +    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
     1.9    in (Term.dest_Const (Term.head_of lhs), rhs) end
    1.10    handle TERM (msg, _) => error msg;
    1.11