equal
deleted
inserted
replaced
354 val _ = name <> "" orelse error "add_expand_thms: unnamed theorem"; |
354 val _ = name <> "" orelse error "add_expand_thms: unnamed theorem"; |
355 |
355 |
356 val is_def = |
356 val is_def = |
357 (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of |
357 (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of |
358 (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts) |
358 (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts) |
359 andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name) |
359 andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.axiom thy) name) |
360 | _ => false) handle TERM _ => false; |
360 | _ => false) handle TERM _ => false; |
361 in |
361 in |
362 (ExtractionData.put (if is_def then |
362 (ExtractionData.put (if is_def then |
363 {realizes_eqns = realizes_eqns, |
363 {realizes_eqns = realizes_eqns, |
364 typeof_eqns = add_rule (([], |
364 typeof_eqns = add_rule (([], |