equal
deleted
inserted
replaced
118 fun rep_datatype_i elim induct case_eqns recursor_eqns thy = |
118 fun rep_datatype_i elim induct case_eqns recursor_eqns thy = |
119 let |
119 let |
120 (*analyze the LHS of a case equation to get a constructor*) |
120 (*analyze the LHS of a case equation to get a constructor*) |
121 fun const_of (Const("op =", _) $ (_ $ c) $ _) = c |
121 fun const_of (Const("op =", _) $ (_ $ c) $ _) = c |
122 | const_of eqn = error ("Ill-formed case equation: " ^ |
122 | const_of eqn = error ("Ill-formed case equation: " ^ |
123 Sign.string_of_term thy eqn); |
123 Syntax.string_of_term_global thy eqn); |
124 |
124 |
125 val constructors = |
125 val constructors = |
126 map (head_of o const_of o FOLogic.dest_Trueprop o |
126 map (head_of o const_of o FOLogic.dest_Trueprop o |
127 #prop o rep_thm) case_eqns; |
127 #prop o rep_thm) case_eqns; |
128 |
128 |