equal
deleted
inserted
replaced
485 end; |
485 end; |
486 |
486 |
487 fun string_of_terms sign terms = |
487 fun string_of_terms sign terms = |
488 let fun make_string sign [] = "" | |
488 let fun make_string sign [] = "" | |
489 make_string sign (trm::list) = |
489 make_string sign (trm::list) = |
490 Sign.string_of_term sign trm ^ "\n" ^ make_string sign list |
490 Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list |
491 in |
491 in |
492 PrintMode.setmp ["Mucke"] (make_string sign) terms |
492 PrintMode.setmp ["Mucke"] (make_string sign) terms |
493 end; |
493 end; |
494 |
494 |
495 fun callmc s = |
495 fun callmc s = |
687 fun rc_in_term sg tl (a $ b) l x 0 = |
687 fun rc_in_term sg tl (a $ b) l x 0 = |
688 (replace_case sg tl a 0) $ (rc_in_termlist sg tl l x) | |
688 (replace_case sg tl a 0) $ (rc_in_termlist sg tl l x) | |
689 rc_in_term sg tl _ l x 0 = rc_in_termlist sg tl l x | |
689 rc_in_term sg tl _ l x 0 = rc_in_termlist sg tl l x | |
690 rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) | |
690 rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) | |
691 rc_in_term sg _ trm _ _ n = |
691 rc_in_term sg _ trm _ _ n = |
692 error("malformed term for case-replacement: " ^ (Sign.string_of_term sg trm)); |
692 error("malformed term for case-replacement: " ^ (Syntax.string_of_term_global sg trm)); |
693 val (bv,n) = check_case sg tl (a $ b); |
693 val (bv,n) = check_case sg tl (a $ b); |
694 in |
694 in |
695 if (bv) then |
695 if (bv) then |
696 (let |
696 (let |
697 val t = (replace_case sg tl a n) |
697 val t = (replace_case sg tl a n) |
990 extract_type_names_prems sg (a::b) = |
990 extract_type_names_prems sg (a::b) = |
991 let |
991 let |
992 fun analyze_types sg [] = [] | |
992 fun analyze_types sg [] = [] | |
993 analyze_types sg [Type(a,[])] = |
993 analyze_types sg [Type(a,[])] = |
994 (let |
994 (let |
995 val s = (Sign.string_of_typ sg (Type(a,[]))) |
995 val s = (Syntax.string_of_typ_global sg (Type(a,[]))) |
996 in |
996 in |
997 (if (s="bool") then ([]) else ([Type(a,[])])) |
997 (if (s="bool") then ([]) else ([Type(a,[])])) |
998 end) | |
998 end) | |
999 analyze_types sg [Type("*",l)] = analyze_types sg l | |
999 analyze_types sg [Type("*",l)] = analyze_types sg l | |
1000 analyze_types sg [Type("fun",l)] = analyze_types sg l | |
1000 analyze_types sg [Type("fun",l)] = analyze_types sg l | |