equal
deleted
inserted
replaced
35 ("Extra variables on RHS in definition of " ^ name) |
35 ("Extra variables on RHS in definition of " ^ name) |
36 in (name ^ "_def", |
36 in (name ^ "_def", |
37 flatten_term sign (Logic.mk_equals (lhs,rhs))) |
37 flatten_term sign (Logic.mk_equals (lhs,rhs))) |
38 end; |
38 end; |
39 |
39 |
40 (*export to Pure/sign? Used in Provers/simp.ML...*) |
|
41 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a); |
40 fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a); |
42 |
41 |
43 (*export to Pure/library? *) |
42 (*export to Pure/library? *) |
44 fun assert_all pred l msg_fn = |
43 fun assert_all pred l msg_fn = |
45 let fun asl [] = () |
44 let fun asl [] = () |