src/Pure/theory.ML
changeset 9537 7e0ba737f98e
parent 9332 ff3a86a00ea5
child 9629 50f1c4222aea
equal deleted inserted replaced
9536:b79b002f32ae 9537:7e0ba737f98e
   244   let
   244   let
   245     val (t, T, _) = Sign.certify_term sg raw_tm
   245     val (t, T, _) = Sign.certify_term sg raw_tm
   246       handle TYPE (msg, _, _) => error msg
   246       handle TYPE (msg, _, _) => error msg
   247            | TERM (msg, _) => error msg;
   247            | TERM (msg, _) => error msg;
   248   in
   248   in
       
   249     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   249     assert (T = propT) "Term not of type prop";
   250     assert (T = propT) "Term not of type prop";
   250     (name, no_vars t)
   251     (name, no_vars t)
   251   end
   252   end
   252   handle ERROR => err_in_axm name;
   253   handle ERROR => err_in_axm name;
   253 
   254