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