equal
deleted
inserted
replaced
579 space_implode " -> " (map |
579 space_implode " -> " (map |
580 (fn NONE => "X" | SOME k' => string_of_int k') |
580 (fn NONE => "X" | SOME k' => string_of_int k') |
581 (ks @ [SOME k]))) arities)); |
581 (ks @ [SOME k]))) arities)); |
582 |
582 |
583 fun prep_intrs intrs = |
583 fun prep_intrs intrs = |
584 map (Codegen.rename_term o #prop o rep_thm o Drule.export_without_context) intrs; |
584 map (Codegen.rename_term o Thm.prop_of o Drule.export_without_context) intrs; |
585 |
585 |
586 fun constrain cs [] = [] |
586 fun constrain cs [] = [] |
587 | constrain cs ((s, xs) :: ys) = |
587 | constrain cs ((s, xs) :: ys) = |
588 (s, |
588 (s, |
589 (case AList.lookup (op =) cs (s : string) of |
589 (case AList.lookup (op =) cs (s : string) of |