equal
deleted
inserted
replaced
103 fun fixed_judgment thy x = |
103 fun fixed_judgment thy x = |
104 let (*be robust wrt. low-level errors*) |
104 let (*be robust wrt. low-level errors*) |
105 val c = judgment_name thy; |
105 val c = judgment_name thy; |
106 val aT = TFree ("'a", []); |
106 val aT = TFree ("'a", []); |
107 val T = |
107 val T = |
108 if_none (Sign.const_type thy c) (aT --> propT) |
108 the_default (aT --> propT) (Sign.const_type thy c) |
109 |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S)); |
109 |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S)); |
110 val U = Term.domain_type T handle Match => aT; |
110 val U = Term.domain_type T handle Match => aT; |
111 in Const (c, T) $ Free (x, U) end; |
111 in Const (c, T) $ Free (x, U) end; |
112 |
112 |
113 fun ensure_propT thy t = |
113 fun ensure_propT thy t = |