src/HOL/Tools/record.ML
changeset 47234 0599911c2bf5
parent 46990 63fae4a2cc65
child 47783 0eadfb89badb
equal deleted inserted replaced
47233:5d89a3afcebd 47234:0599911c2bf5
  1312       let
  1312       let
  1313         fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1313         fun mkeq (lr, Teq, (sel, Tsel), x) i =
  1314           if is_selector thy sel then
  1314           if is_selector thy sel then
  1315             let
  1315             let
  1316               val x' =
  1316               val x' =
  1317                 if not (loose_bvar1 (x, 0))
  1317                 if not (Term.is_dependent x)
  1318                 then Free ("x" ^ string_of_int i, range_type Tsel)
  1318                 then Free ("x" ^ string_of_int i, range_type Tsel)
  1319                 else raise TERM ("", [x]);
  1319                 else raise TERM ("", [x]);
  1320               val sel' = Const (sel, Tsel) $ Bound 0;
  1320               val sel' = Const (sel, Tsel) $ Bound 0;
  1321               val (l, r) = if lr then (sel', x') else (x', sel');
  1321               val (l, r) = if lr then (sel', x') else (x', sel');
  1322             in Const (@{const_name HOL.eq}, Teq) $ l $ r end
  1322             in Const (@{const_name HOL.eq}, Teq) $ l $ r end