equal
deleted
inserted
replaced
16 struct |
16 struct |
17 |
17 |
18 exception RecError of string; |
18 exception RecError of string; |
19 |
19 |
20 (*Remove outer Trueprop and equality sign*) |
20 (*Remove outer Trueprop and equality sign*) |
21 val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop; |
21 val dest_eqn = FOLogic.dest_eq o \<^dest_judgment>; |
22 |
22 |
23 fun primrec_err s = error ("Primrec definition error:\n" ^ s); |
23 fun primrec_err s = error ("Primrec definition error:\n" ^ s); |
24 |
24 |
25 fun primrec_eq_err sign s eq = |
25 fun primrec_eq_err sign s eq = |
26 primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq); |
26 primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq); |