equal
deleted
inserted
replaced
76 val opts = [] |> type_enc <> partial_typesN ? cons type_enc |
76 val opts = [] |> type_enc <> partial_typesN ? cons type_enc |
77 |> lam_trans <> metis_default_lam_trans ? cons lam_trans |
77 |> lam_trans <> metis_default_lam_trans ? cons lam_trans |
78 in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end |
78 in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end |
79 |
79 |
80 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s |
80 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s |
81 | term_name' t = "" |
81 | term_name' _ = "" |
82 |
82 |
83 fun lambda' v = Term.lambda_name (term_name' v, v) |
83 fun lambda' v = Term.lambda_name (term_name' v, v) |
84 |
84 |
85 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t |
85 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t |
86 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t |
86 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t |