641 (case vs of |
641 (case vs of |
642 [] => raise error ("pbl_ids' Tools.nam called with []") |
642 [] => raise error ("pbl_ids' Tools.nam called with []") |
643 | [t] => (case t of (*eg. eps=#0*) |
643 | [t] => (case t of (*eg. eps=#0*) |
644 (Const ("op =",_) $ l $ r) => [r,l] |
644 (Const ("op =",_) $ l $ r) => [r,l] |
645 | _ => raise error ("pbl_ids' Tools.nam: no equality " |
645 | _ => raise error ("pbl_ids' Tools.nam: no equality " |
646 ^(Syntax.string_of_term (ctxt_Isac"")t))) |
646 ^(Syntax.string_of_term (thy2ctxt' "Isac")t))) |
647 | vs' => vs (*14.9.01: ???TODO *)) |
647 | vs' => vs (*14.9.01: ???TODO *)) |
648 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs |
648 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.una",_)]))) vs = vs |
649 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs |
649 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.unl",_)]))) vs = vs |
650 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs |
650 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.str",_)]))) vs = vs |
651 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs |
651 | pbl_ids' (Const(_,Type("fun",[_,Type("Tools.toreal",_)]))) vs = vs |