112 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of; |
112 val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of; |
113 |
113 |
114 |
114 |
115 (** reading of instantiations **) |
115 (** reading of instantiations **) |
116 |
116 |
117 fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v |
|
118 | _ => error("Lexical error in variable name " ^ quote (implode cs)); |
|
119 |
|
120 fun absent ixn = |
117 fun absent ixn = |
121 error("No such variable in term: " ^ Syntax.string_of_vname ixn); |
118 error("No such variable in term: " ^ Syntax.string_of_vname ixn); |
122 |
119 |
123 fun inst_failure ixn = |
120 fun inst_failure ixn = |
124 error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails"); |
121 error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails"); |
125 |
122 |
126 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = |
123 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = |
127 let val {tsig,...} = Sign.rep_sg sign |
124 let val {tsig,...} = Sign.rep_sg sign |
128 fun split([],tvs,vs) = (tvs,vs) |
125 fun split([],tvs,vs) = (tvs,vs) |
129 | split((sv,st)::l,tvs,vs) = (case explode sv of |
126 | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of |
130 "'"::cs => split(l,(indexname cs,st)::tvs,vs) |
127 "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs) |
131 | cs => split(l,tvs,(indexname cs,st)::vs)); |
128 | cs => split(l,tvs,(Syntax.indexname cs,st)::vs)); |
132 val (tvs,vs) = split(insts,[],[]); |
129 val (tvs,vs) = split(insts,[],[]); |
133 fun readT((a,i),st) = |
130 fun readT((a,i),st) = |
134 let val ixn = ("'" ^ a,i); |
131 let val ixn = ("'" ^ a,i); |
135 val S = case rsorts ixn of Some S => S | None => absent ixn; |
132 val S = case rsorts ixn of Some S => S | None => absent ixn; |
136 val T = Sign.read_typ (sign,sorts) st; |
133 val T = Sign.read_typ (sign,sorts) st; |