src/Pure/theory.ML
changeset 9629 50f1c4222aea
parent 9537 7e0ba737f98e
child 10403 2955ee2424ce
equal deleted inserted replaced
9628:53a62fd8b2dc 9629:50f1c4222aea
   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     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   250     assert (T = propT) "Term not of type prop";
   250     assert (T = propT) "Term not of type prop";
   251     (name, no_vars t)
   251     (name, no_vars t)
   252   end
   252   end;
   253   handle ERROR => err_in_axm name;
       
   254 
   253 
   255 (*some duplication of code with read_def_cterm*)
   254 (*some duplication of code with read_def_cterm*)
   256 fun read_def_axm (sg, types, sorts) used (name, str) =
   255 fun read_def_axm (sg, types, sorts) used (name, str) =
   257   let
   256   let
   258     val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;
   257     val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;